coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] omega's term, Yakov Zaytsev
- Re: [Coq-Club] omega's term,
Adam Chlipala
- Re: [Coq-Club] omega's term,
Yakov Zaytsev
- Re: [Coq-Club] omega's term, Adam Chlipala
- Re: [Coq-Club] omega's term,
Yakov Zaytsev
- Re: [Coq-Club] omega's term,
Adam Chlipala
Archive powered by MhonArc 2.6.16.