blob: 229df9377304c01b6c04f0e7b09c0f3826f3f471 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Set Universe Polymorphism.
Module OK.
Inductive one@{i j} : Type@{i} :=
with two : Type@{j} := .
Check one@{Set Type} : Set.
Fail Check two@{Set Type} : Set.
End OK.
Module Bad.
Fail Inductive one :=
with two@{i +} : Type@{i} := .
Fail Inductive one@{i +} :=
with two@{i +} := .
End Bad.
|
