coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: vincent.chatel AT transport.alstom.com
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Set or Type
- Date: Wed, 25 Sep 2002 13:48:02 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I'm using the following construction :
Require Arith.
Set Implicit Arguments.
Inductive listn : nat->Type :=
niln:(listn O)
| consn :(A:Type)(n:nat) A->(listn n)->(listn (S n)).
When I try to build listn with elements of type listn :
Parameter X:Type.
Parameter x1,x2:X.
Definition l1 := (consn x1 (consn x2 niln)). (* OK *)
Definition l2 := (consn l1 niln)
Coq answers "Error: Universe Inconsistency"
But if I change "Type" by "Set" :
Inductive listn : nat->Set :=
niln:(listn O)
| consn :(A:Set)(n:nat) A->(listn n)->(listn (S n)).
l2 is defined.
Why I cannot build listn of listn with "Type".
- [Coq-Club] Set or Type, vincent . chatel
- Re: [Coq-Club] Set or Type, Benjamin Werner
Archive powered by MhonArc 2.6.16.