coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yucheng Zhang <yczhang89 AT gmail.com>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] inserting a partially applied hypothesis
- Date: Tue, 22 Jan 2013 04:08:07 +0800
On Jan 22, 2013, at 4:07 AM, AUGER Cédric
<sedrikov AT gmail.com>
wrote:
> Check the "assert" tactics to find out all the variants (mainly set and
> pose). There is also the "cut" tactic. It is not the same as assert,
> but desserves some similar goal.
There is also a 'specialize (H x0)' tactic, if the old hypothesis 'forall x y,
P x y' is not needed any more.
- [Coq-Club] inserting a partially applied hypothesis, Leonardo Rodriguez, 01/21/2013
- Re: [Coq-Club] inserting a partially applied hypothesis, AUGER Cédric, 01/21/2013
- Re: [Coq-Club] inserting a partially applied hypothesis, Yucheng Zhang, 01/21/2013
- Re: [Coq-Club] inserting a partially applied hypothesis, AUGER Cédric, 01/21/2013
Archive powered by MHonArc 2.6.18.