Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] inserting a partially applied hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inserting a partially applied hypothesis


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page