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
|
Universe i j.
Goal False.
Proof.
Check Type@{i} : Type@{j}.
Fail constr_eq_strict Type@{i} Type@{j}.
assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
Fail constr_eq_strict Type@{i} Type@{j}.
constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
constr_eq_strict Type@{i} Type@{j}.
Fail Check Type@{i} : Type@{j}.
Fail constr_eq Prop Set.
Fail constr_eq Prop Type.
Fail constr_eq_strict Type Type.
constr_eq Type Type.
constr_eq_strict Set Set.
constr_eq Set Set.
constr_eq Prop Prop.
let x := constr:(Type) in constr_eq_strict x x.
let x := constr:(Type) in constr_eq x x.
Fail lazymatch type of prod with
| ?A -> ?B -> _ => constr_eq_strict A B
end.
lazymatch type of prod with
| ?A -> ?B -> _ => constr_eq A B
end.
lazymatch type of prod with
| ?A -> ?B -> ?C => constr_eq A C
end.
Abort.
|
