Patrick Nicodemus (May 06 2022 at 22:57): Patrick Nicodemus (May 06 2022 at 22:57):How can I use Ltac to do something along the lines of "for each hypothesis matching this pattern, do this".
Patrick Nicodemus (May 06 2022 at 22:59):I know I have to use match goal but I think that match goal only finds the first hypothesis matching the pattern and then moves on. I want to do this to all hypotheses matching the pattern.
Notification Bot (May 06 2022 at 23:15):Patrick Nicodemus has marked this topic as resolved.
Patrick Nicodemus (May 06 2022 at 23:16):nvm I think I found the answer in the coq docs, I can do this with
match goal with
| [ H : pattern |- _ ] => // do what I want ; fail
| _ => idtac
end
but lmk if there's a better way or if this is not like, idiomatic
Paolo Giarrusso (May 07 2022 at 06:01):fail will undo what you did in the branch. I'd add repeat around match goal, but then you need to avoid infinite loops
Patrick Nicodemus (May 07 2022 at 06:06):Paolo Giarrusso said:
fail will undo what you did in the branch. I'd add repeat around match goal, but then you need to avoid infinite loops
Ah, ok, I see. Yeah I am running into what I think is an ltac bug in this specific context ( https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Match.20on.20type.20of.20t.20-.20bug.3F )
which makes the problem of avoiding the loop harder. I was hoping there was some native command to just go through everything once.
Last updated: Apr 18 2024 at 11:02 UTC