Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]Matching let expressions in Ltac

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Matching let expressions in Ltac


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

Definition test : (let (a,b) := (0, 1) in a=0).


Compound lets aren't compiled into real lets.  Try this instead:

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.





Archive powered by MhonArc 2.6.16.

Top of Page