coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: Gert Smolka <smolka AT ps.uni-saarland.de>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] functional induction, Equations plugin
- Date: Tue, 27 Nov 2012 13:12:55 +0100
I realize that my first answer to Gert Smolka was not cced to this
list and that it makes my other messages difficult to understand.
I copy it here and ask again: Has anyone ever used successfully
"induction X" where X is something else than a variable?
Best regards,
Pierre
> Indeed, functional induction is similar to induction (it *is* a call
> to induction actually): it mostly works on variables. We could modify
> functional induction (and induction actually) to always do a
> "remember" when applied to non variable terms. I wonder if this would
> break some strange usage of induction.
>
> Has anyone ever used successfully "induction X" where X is something
> else than a variable?
> Best regards,
> Pierre
- Re: [Coq-Club] functional induction, Equations plugin, (continued)
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Message not available
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/27/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
Archive powered by MHonArc 2.6.18.