Hello, is it possible to change that default variable/hypothesis names when using induction instead of constantly having to specify induction t as ...
?
I am afraid that IH
is hard coded but you can always use some ltac to get what you want.
Ltac my_ind n :=
let v := fresh "Hind" n in
induction n as [|n v].
Goal forall m : nat, m = m.
my_ind m.
- trivial.
-
anyway it is good practice to explicitly name your assumptions with induction ... as ...
I see, thank you!
Last updated: Oct 13 2024 at 01:02 UTC