Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Set or Type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Set or Type


chronological Thread 

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".






Archive powered by MhonArc 2.6.16.

Top of Page