If I destruct a thing involving a bool (or remember a bool), the resulting bool will most likely be called b, b0, b1, …; a natural number will be n, …; and so on. Can I access the same name generation mechanism from Ltac? 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?