coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eugene Kirpichov <ekirpichov AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Ltac-matching a "match..with"
- Date: Sat, 30 Jan 2010 00:27:57 +0300
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=eKMvALA+b3gC8sXECAQcOtjx3NhG2turFfqquFCRQ7214ZIu+TxKxcL2Fw60JWIj7W uVyHxP92tFn77fZ8kSWcqIn1QDs7cJNN1X1/5W3Mo3AkavAEKaiDVoUnaN+to3tik/DE FoLnkLjbbRV+ZfRq96EdjbqugKLAxTuxnScQE=
Hello, coq-club.
Suppose I'm proving the following theorem.
Theorem t : forall n, match n with | O => O | S x => S x end = n.
intros n.
(* Here I could just do "destruct n", but I'd like to do that automatically
*)
match goal with [ |- match ?n with _ end ] => destruct n end.
This doesn't work. Replacing _ with _ => _ doesn't work, either, and
neither does work anything that I managed to invent.
Is there a way to achieve what I'm trying to do? namely, say,
"destruct" all variables that are being the head of a match?
--
Eugene Kirpichov
Web IR developer, market.yandex.ru
- [Coq-Club] Ltac-matching a "match..with", Eugene Kirpichov
- Re: [Coq-Club] Ltac-matching a "match..with",
Adam Chlipala
- Re: [Coq-Club] Ltac-matching a "match..with",
Eugene Kirpichov
- Re: [Coq-Club] Ltac-matching a "match..with", Adam Chlipala
- Re: [Coq-Club] Ltac-matching a "match..with",
Eugene Kirpichov
- Re: [Coq-Club] Ltac-matching a "match..with",
Adam Chlipala
Archive powered by MhonArc 2.6.16.