Stream: Ltac2

Topic: ✔ `pose proof` in ltac2?


view this post on Zulip Michael Soegtrop (Jun 29 2023 at 12:07):

I wonder if there is an equivalent of Ltac1 pose proof in Ltac2 - that is an opaque variant of pose. I currently use pose, but there are cases where the proof term is so large that the IDEs start to get sluggish, while the type is quite small.

view this post on Zulip Pierre-Marie Pédrot (Jun 29 2023 at 12:10):

pose proof is an alias for assert, so this one should work

view this post on Zulip Pierre-Marie Pédrot (Jun 29 2023 at 12:11):

e.g. pose proof (x := true) and assert (x := true) are literally the same

view this post on Zulip Michael Soegtrop (Jun 29 2023 at 12:22):

Ah I see - I am using assert when I specify the type of a term and pose when I specify the term itself. I didn't know that there is a syntax variant of assert which allows specifying the proof term (I guess that without the x:= one has to say bool instead of true and then supply the true laster).

view this post on Zulip Notification Bot (Jun 29 2023 at 12:22):

Michael Soegtrop has marked this topic as resolved.


Last updated: May 24 2024 at 23:01 UTC