Stream: Coq users

Topic: Register a hand-written induction scheme for `induction`


view this post on Zulip Lef Ioannidis (Oct 09 2023 at 14:05):

I have an inductive predicate F with induction scheme F_ind that is not very useful. I defined a custom induction scheme F_ind' and I would like to replace the autogenerated scheme for my own, as far as the induction tactic is concerned.

Am I remembering wrong there is a way to either,

  1. Delete F_ind and rename F_ind' -> F_ind and the induction tactic will use it.
  2. Use a vernacular command (perhaps Scheme?) to register F_ind' as the default scheme for the induction tactic.

Attached a reproducible example. Thank you.
Ceu.v

view this post on Zulip Dominique Larchey-Wendling (Oct 09 2023 at 14:15):

Unset Elimination Schemes is the command you want to use...

view this post on Zulip Lef Ioannidis (Oct 09 2023 at 14:18):

That is precisely what I want, thank you!


Last updated: Jun 23 2024 at 05:02 UTC