1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
Set Universe Polymorphism. Set Printing Universes.
Module MultiInd.
Section S.
Universe u.
Cumulative Inductive I1 := C1 (_:Type@{u}).
Cumulative Inductive I2 := C2 (_:I1).
End S.
(* !!! should be covariant !!! *)
Fail Cumulative Inductive I3@{*u} := C3 (_:I2@{u}).
Cumulative Inductive I3@{u} := C3 (_:I2@{u}).
(* alternative test without the variance syntax: *)
Fail Check C3@{Type} _ : I3@{Set}. (* should fail but doesn't *)
Check C3@{Set} _ : I3@{Type}.
End MultiInd.
Module WithAxiom.
Section S.
Universe u.
Axiom t : Type@{u}. (* or even a Qed definition *)
Cumulative Inductive I1 := C1 (_:t).
End S.
(* !!! should be invariant !!! *)
Fail Cumulative Inductive I2@{*u} := C2 (_:I1@{u}).
Fail Cumulative Inductive I2@{+u} := C2 (_:I1@{u}).
Cumulative Inductive I2@{u} := C2 (_:I1@{u}).
(* !!! should not work !!! *)
Fail Polymorphic Definition lift_t@{u v|} (x:t@{u}) : t@{v}
:= match (C1@{u} x) : I1@{v} with C1 y => y end.
Fail Polymorphic Definition lift_t@{u v|u < v +} (x:t@{u}) : t@{v}
:= match (C1@{u} x) : I1@{v} with C1 y => y end.
(* sanity check that the above 2 test the right thing *)
Polymorphic Definition lift_t@{u v} (x:t@{u}) : t@{v}
:= match (C1@{u} x) : I1@{v} with C1 y => y end.
End WithAxiom.
Module WithVars.
Module Rel.
Fail Cumulative Inductive foo@{*u +} (X:=Type@{u}) := C (_:X).
Cumulative Inductive foo@{+u +} (X:=Type@{u}) := C (_:X).
End Rel.
Module Var.
Section S.
Let X:=Type.
Cumulative Inductive foo := C (_:X).
End S.
Fail Cumulative Inductive bar@{*u} := C' (_:foo@{u}).
Cumulative Inductive bar@{+u} := C' (_:foo@{u}).
End Var.
End WithVars.
|
