Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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?




Archive powered by MhonArc 2.6.16.

Top of Page