coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stefan Karrmann <sk AT mathematik.uni-ulm.de>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Universe Inconsistency?
- Date: Thu, 21 Oct 2004 21:30:52 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
if the tower of Type is Type_i : Type_{i+1} for all i in N, why does the
following gives an error?
Coq < Print type_of.
type_of = fun (T : Type) (_ : T) => T
: forall T : Type, T -> Type
Argument T is implicit
Argument scopes are [type_scope _]
Coq < Eval compute in (type_of (type_of (Type))).
Error: Universe Inconsistency.
Here the written Type is Type_i for some i in N. Then type_of Type_i is
Type_{i+1} and the final result should be Type_{i+2} of type Type_{i+3}.
Where gets the inconsistency in?
PS: The same happens for Set, nat and O:
Coq < Eval compute in (type_of (type_of (O))).
Error: Universe Inconsistency.
Regards,
--
Stefan Karrmann
"The reasonable man adapts himself to the world; the unreasonable one persists
in trying to adapt the world to himself. Therefore all progress depends on
the unreasonable man."
-- George Bernard Shaw
- [Coq-Club] Universe Inconsistency?, Stefan Karrmann
- Re: [Coq-Club] Universe Inconsistency?,
Hugo Herbelin
- Re: [Coq-Club] Universe Inconsistency?, Randy Pollack
- Re: [Coq-Club] Universe Inconsistency?,
Hugo Herbelin
Archive powered by MhonArc 2.6.16.