coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] match goal with "match ... with", Gyesik Lee
- Re: [Coq-Club] match goal with "match ... with",
Adam Chlipala
Archive powered by MhonArc 2.6.16.