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.
pose proof is an alias for assert, so this one should work
pose proof (x := true) and
assert (x := true) are literally the same
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
Michael Soegtrop has marked this topic as resolved.
Last updated: Nov 29 2023 at 22:01 UTC