Stream: Coq users

Topic: ✔ Basic tactics q

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: Feb 09 2023 at 00:03 UTC