Michael Soegtrop (Jun 29 2023 at 12:07): 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.
Pierre-Marie Pédrot (Jun 29 2023 at 12:10):pose proof is an alias for assert, so this one should work
Pierre-Marie Pédrot (Jun 29 2023 at 12:11):e.g. pose proof (x := true) and assert (x := true) are literally the same
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).
Notification Bot (Jun 29 2023 at 12:22):Michael Soegtrop has marked this topic as resolved.
Last updated: Oct 08 2024 at 15:02 UTC