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
IHis 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 04 2023 at 23:01 UTC