blob: 42bdb076b6ca40450855ca5173804230851a86fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Hurkens.
Universes i j k.
Module Type T.
Parameter T1 : Type@{i+1}.
Parameter e : Type@{j} = T1 : Type@{k}.
End T.
Module M.
Definition T1 := Type@{j}.
Definition e : Type@{j} = T1 : Type@{k} := eq_refl.
End M.
Module F (A:T).
Definition bad := TypeNeqSmallType.paradox _ A.e.
End F.
Set Printing Universes.
Fail Module X := F M.
(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *)
|
