The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Benjamin Werner wrote:

> Hi,

> Just do "Print existS". Actually it is the single constructor of SigS  
> which is a pair of two objects of kind Set, but where the type of the  
> second component depends upon the value of the first. There used to  
> be some concrete syntax like {x:A|P} for it, but for some reason it  
> seems switched off.
Well, the notation {x:A & B} is an abreviation only for (sigS A (fun x:A 
=> P)).


By the way, sigS types are presented in the book as "Nested Subset 
types" (9.1.2). The main example in
which this type is used is euclidean division with the type
{q:Z & {r:Z | a= b * q + r}}

Pierre




> Anyway, since existS is a constructor, the first equality implies  
> that A=Apply M N, which, I imagine is false.
> So inversion H14 should make it.
>
> Cheers,
>
>
> Benjamin
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club