coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] match goal with "match ... with"

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Adam Chlipala <adam AT chlipala.net>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] match goal with "match ... with"
Date: Fri, 2 Jul 2010 22:17:52 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=j9aUOnVBJ0yLu50jL78yKzclv5Uu30NmSpkrx1RKgPk0Zi3c9zt4Wl/ij3yz7iaz81 fQnP7KWww7ZUGMRIM4Q3GPUdqUkLJQtTIENvb5LmYAHjeMYUX5Nt5LJ5PVv60v+2zMXK XEC9Pxe56ncX5kJe7+xcVXco3QCHmrv/5GNhA=

> For now, you need to supply every pattern-match case, in enough detail to
> make clear which type you're matching on.  It gets bothersomely verbose and
> prevents genericity, but it makes some sense if you look at the internal
> representation of Gallina terms.

Does this mean that

>>   match goal with
>>      | |- context [ match ?T with | _ =>  _ end ] =>  idtac
>>   end

can be used only in a proof, and not as a standing-alone tactic with a name?

[Coq-Club] match goal with "match ... with", Gyesik Lee
- Re: [Coq-Club] match goal with "match ... with", Adam Chlipala
  - Re: [Coq-Club] match goal with "match ... with", Gyesik Lee
    - Re: [Coq-Club] match goal with "match ... with", Adam Chlipala