coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!
- [Coq-Club] Ltac: destruct let if not single var, t x, 08/21/2013
- Re: [Coq-Club] Ltac: destruct let if not single var, Valentin Robert, 08/21/2013
- Re: [Coq-Club] Ltac: destruct let if not single var, Adam Chlipala, 08/21/2013
Archive powered by MHonArc 2.6.18.