The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Thu, 18 Oct 2007 15:16:54 -0700 (PDT), gang chen
<gangchen_sh AT yahoo.com>
 a écrit:
> 
>  Here is the statement of treesort in Heap:
> 
>     forall l:list A, {m : list A | sort leA m & permutation _ eqA_dec l m}.
>   
> Is the use '&' here a bug ? I suspect it should be '/\'.
> 

No, this notation refers to sig2 which has a better elimination
principle than sig + conjonction. See the difference:

Hypothesis H: {m:nat | m=0 & m=1}.   
Hypothesis H': {m:nat | m=0 /\ m=1}.   
Goal False.

 elim H.    gives  forall x : nat, x = 0 -> x = 1 -> False
whereas 
 elim H'    gives   forall x : nat, x = 0 /\ x = 1 -> False


Cheers,
Pierre Courtieu