coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT cs.berkeley.edu>
- To: Sean Wilson <sean.wilson AT ed.ac.uk>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club]Matching let expressions in Ltac
- Date: Thu, 20 Jul 2006 10:58:13 -0700
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Sean Wilson wrote:
I wish to write a Coq tactic that matches goals that are similar to that of the following statement:Compound lets aren't compiled into real lets. Try this instead:
Definition test : (let (a,b) := (0, 1) in a=0).
Ltac letPair :=
match goal with
| [ |- context[ match _ with (_, _) => _ end ] ] => idtac
end.
Also, how would I go about outputting matched patterns in Ltac for debug purposes?To make available expression E for perusal, you can do something like "assert (E = E)" in your tactic. Pretty hackish, but I don't know a better way.
- [Coq-Club]Matching let expressions in Ltac, Sean Wilson
- Re: [Coq-Club]Matching let expressions in Ltac, Adam Chlipala
Archive powered by MhonArc 2.6.16.