destruct a thing involving a
bool), the resulting bool will most likely be called
b1, …; a natural number will be
n, …; and so on. Can I access the same name generation mechanism from
fresh defaults to
H no matter what, I can only pass in a name or string (or several) to use in place of
H. What if I don’t have any?
The concrete context I currently want that in is writing a
remember variant that flips the equality. (Both
rewrite and most library theorems expect the equality to have the opposite direction from what
remember generates, and I don’t want to deal with using
rewrite <- or
symmetry in or whatever all. the. time.)
So far I have:
Tactic Notation "remember'" constr(t) "as" ident(x) "eqn" ":" ident(H) := (* NB: using "eqn:" instead of "eqn" ":" in the Notation messes up the grammar *) remember t as x eqn:H; symmetry in H. Tactic Notation "remember'" constr(t) "as" ident(x) := let H := fresh "Heq" x in remember' t as x eqn:H.
Now I’d also like to have a
Tactic Notation "remember'" constr(t) := … that makes nice names like
remember does, but I don’t know how to access the name generation mechanism. Any pointers?