Patrick Nicodemus has marked this topic as resolved.
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
fail will undo what you did in the branch. I'd add repeat around match goal, but then you need to avoid infinite loops
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: Feb 09 2023 at 00:03 UTC