The Coq mailing list

["Kouskoulas, Yanni A." <Yanni.Kouskoulas AT jhuapl.edu>]

> One of the trivial cases whose description was left out from the book is
> this:
> s = Prop
> s' = s'' = Set
> 
>        E,$B&#(B |- A:Prop      E,$B&#(B::(a:A) |- B:Set
>         ----------------------------------
>             E,$B&#(B |- $B"O(Ba:A,B:Set

Hi. The types of partial functions depend on this triplet, i.e. in

forall n:nat, [0<n -> nat]

the bracketed part uses it, see p 94 in the text.

Also, this triplet is very useful for making strongly specified functions 
that return values along with certificates or guarantees about the data they 
hold. The sig type is an example, see p. 252; its constructor has the type

forall (A:Set) (P:A->Prop) (x:A), [P x -> sig A P]

again the bracketed part depends on this rule.

-Yanni