Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] omega's term

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] omega's term


chronological Thread 
  • From: Adam Chlipala <adam AT chlipala.net>
  • To: Yakov Zaytsev <yakov AT yakov.cc>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] omega's term
  • Date: Sat, 20 Mar 2010 09:30:16 -0400

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.



Archive powered by MhonArc 2.6.16.

Top of Page