The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Yakov Zaytsev wrote:
> (*Now I'm confused :-). [Zle] is defined as follows.
> Why then it does not have type [Zle : Z ->  Z ->  Prop ->  Prop] because of 
> application of [not]?*)
> Print Zle.
> (* Zle = fun x y : Z =>  not (eq (Zcompare x y) Gt) *)
> (*      : Z ->  Z ->  Prop *)
>    

Why is this type surprising?  Perhaps printing the definition of [not] 
would help.  A critical part of this is that [Prop] does not behave like 
a Haskell type of Booleans; rather, it's more like the Haskell kind "*", 
the type of types.