Stream: Coq users

Topic: ✔ Basic tactics q


view this post on Zulip Notification Bot (May 06 2022 at 23:15):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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