Brandon Moore (Dec 18 2020 at 23:45): Brandon Moore (Dec 18 2020 at 23:45):It seems induction using always names the induction hypotheses based on the type of the term being examined, while a plain induction sometimes gives it a short name (at least when doing induction over a variable). Is there any way to change the default name, or will I need as as clause at every use?
I tried to suggest a name in the definition of the induction lemma by using an unnecessary forall to bind the induction hypothesis, but that didn't help. (I suspect Coq doesn't remember the name if you write a not-actually-dependent parameter with forall rather than ->).
Pierre Courtieu (Dec 23 2020 at 17:50):This may be overkill but you can have a look at my librarie LibHyps (https://github.com/Matafou/LibHyps, installable with opam). It defines a generic customizable auto naming scheme, together with a tactical (default syntax is an exclamation point before any tactic which renames any "new" hypothesis after the tactic. Customization is done by means of ltac functions.
Once installed try the demo file https://github.com/Matafou/LibHyps/blob/master/LibHyps/LibHypsDemo.v.
Last updated: Oct 08 2024 at 16:02 UTC