coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>, homotopytypetheory <homotopytypetheory AT googlegroups.com>
- Cc: Vladimir Voevodsky <vladimir AT ias.edu>
- Subject: Re: [Coq-Club] intros up to ident?
- Date: Sat, 07 Feb 2015 15:07:54 +0000
Hi, I think "intros until n" is what you need.
Note that if the variable has no name you can also do intros until i where i is the number of dependent hypothesis you want to introduce.
P.
Le sam. 7 févr. 2015 à 16:01, Vladimir Voevodsky <vladimir AT ias.edu> a écrit :
Hello,
is there a nice way to ask Coq to do the intros up to (and including) the variable whose name is ident?
E.g. I may have many parameters in a lemma and one of them in the middle is n and I want to do induction in n after having introduced the variables up to n but not the ones after n.
At the moment I say “intros ident_1 …. ident_i n.” but it would produce less fragile code if I could say “intros_up_to n.”
Vladimir.
- [Coq-Club] intros up to ident?, Vladimir Voevodsky, 02/07/2015
- Re: [Coq-Club] intros up to ident?, Pierre Courtieu, 02/07/2015
- Re: [Coq-Club] [HoTT] intros up to ident?, Frédéric Blanqui, 02/07/2015
- Re: [Coq-Club] intros up to ident?, Anthony Bordg, 02/08/2015
Archive powered by MHonArc 2.6.18.