The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

Le jeudi 18 octobre 2007 à 15:16 -0700, gang chen 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. In fact, the syntax { _ | _ & _ } is a notation for the sig2 type:

Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
    exist2 : forall x:A, P x -> Q x -> sig2 P Q.

Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A =>
Q)) : type_scope.

sig2 and its notation are defined in the Datatypes.v file in the
standard library.

-- 
Jean-Marc Notin 
<notin AT lix.polytechnique.fr>