Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ltac: destruct let if not single var

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac: destruct let if not single var


Chronological Thread 
  • From: Valentin Robert <valentin.robert.42 AT gmail.com>
  • To: t x <txrev319 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Ltac: destruct let if not single var
  • Date: Wed, 21 Aug 2013 12:19:18 +0100

I believe you can use something like:

if is_var lhs then idtac else destruct rhs

- Valentin

On Wed, Aug 21, 2013 at 12:02 PM, t x
<txrev319 AT gmail.com>
wrote:
> Hi,
>
> I'm trying to figure out how to write the following Ltac:
>
> match goal with:
> | |- context[ let ?lhs := ?rhs in _ ] => ?????
> end
>
> now, if "lhs" is something like (a::b) or (x,y) or (Constructor t u z) I
> would like to "destruct rhs"
>
> if "lhs" is a single varaible, I don't want to "destruct rhs"
>
> Is there a way to phrase this, to basically say "lhs is not a single var"?
>
> Thanks!



Archive powered by MHonArc 2.6.18.

Top of Page