coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] interactively constructing witnesses of sig types

From: Taral <taralx AT gmail.com>
To: Sean Wilson <sean.wilson AT ed.ac.uk>
Cc: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] interactively constructing witnesses of sig types
Date: Thu, 5 Mar 2009 13:58:36 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=Z5snxsD9sKgOvr9jgB2zx8p5CTVFq456404x4NnhucbI/LgO0Tmv72u2/8xvv32g0h FLuhGK1UIbymdR0I2x//NmWN51bycsL8HhX/4Qcgq4KLVHX6k4artnvaxp4GWMVpHEhy n6PN8ZHcFFo7Xh2bMGkeHltQjEhgBRqdbcIfw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Mar 5, 2009 at 11:33 AM, Sean Wilson
<sean.wilson AT ed.ac.uk>
wrote:
> You can use the "assert" tactic to state what type of term you want to
> construct and use "exists" to make use of (x, x0). You can then
> interactively
> construct the proof part of your term:

Unfortunately this fails because the asserted term is not transparent
and thus cannot be destructed by "gen (spec_and ...)".

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] interactively constructing witnesses of sig types, Keiko Nakata
- Re: [Coq-Club] interactively constructing witnesses of sig types, Taral
- Re: [Coq-Club] interactively constructing witnesses of sig types, Sean Wilson
  - Re: [Coq-Club] interactively constructing witnesses of sig types, Taral