Stream: Coq users

Topic: Changing default names when using induction


view this post on Zulip Fernando Chu (Apr 18 2023 at 14:15):

Hello, is it possible to change that default variable/hypothesis names when using induction instead of constantly having to specify induction t as ...?

view this post on Zulip Laurent Théry (Apr 18 2023 at 15:15):

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 ...

view this post on Zulip Fernando Chu (Apr 18 2023 at 15:51):

I see, thank you!


Last updated: Oct 13 2024 at 01:02 UTC