The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Since we're on the topic of pattern matching, another trick I recently
learned was this:  I think it is well known you can look for local
definitions in your match like this...

match goal with
| a := _ |- _ => ...
end.

But how do you ensure that a matched hypothesis is *not* as local
definition?  Like this...

match goal with
| a: _ |- _ =>
    let e := eval compute in a in
    constr_eq a e;
    ...
end.

 - Aaron

On Wed, Feb 23, 2011 at 3:58 PM, Thomas Braibant
<thomas.braibant AT gmail.com>
 wrote:
> On Wed, Feb 23, 2011 at 9:39 PM, Aaron Bohannon 
>Â <bohannon AT cis.upenn.edu>
>  wrote:
>> Alternatively, instead of using a nested match, you can use
>> "constr_eq", which compares the ASTs of the terms.  So you can do
>> something like this:
>>
>> match goal with
>> | v : T ?n |- context name [?v1] =>  constr_eq v v1; idtac v
>> end.
>>
>
> Nice solution, and thanks to both.
>
> Thomas
>