Stream: Coq users

Topic: elim with induction principle

view this post on Zulip Ineol (Jul 13 2023 at 15:11):

Hi, is there a way to use the ssreflect elim tactic with a custom induction principle, like induction k using my_ind?

view this post on Zulip Karl Palmskog (Jul 13 2023 at 15:12):

elim/my_ind: t

view this post on Zulip Ana de Almeida Borges (Jul 13 2023 at 15:14):

See https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#interpreting-eliminations for details

view this post on Zulip Ineol (Jul 13 2023 at 15:15):

Thank you both! I wasn't looking in the right spot

Last updated: Oct 13 2024 at 01:02 UTC