blob: 6faec0765e01b1c91d7424945bce0d097dbad550 (
plain)
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
|
(* Set Primitive Projections. *)
Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
Arguments bar {_} _ {_}.
Instance: forall A a, @foo A a.
intros; constructor.
abstract reflexivity.
Defined.
Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
Proof.
Check (bar Set).
Check (bar (fun _ : Set => Set)).
Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
Abort.
Module A.
Universes i j.
Constraint i < j.
Variable foo : Type@{i}.
Goal Type@{i}.
Fail let t := constr:(Type@{j}) in
change Type with t.
Abort.
Goal Type@{j}.
Fail let t := constr:(Type@{i}) in
change Type with t.
let t := constr:(Type@{i}) in
change t. exact foo.
Defined.
End A.
|
