blob: a2bfbafe06403586be6bc7489d0dea2aa880a09c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Set Primitive Projections.
Record toto : Type := Toto {
toto1 : Type;
toto2 : toto1 -> Type
}.
Record tata := Tata {
tata1 : Type
}.
Canonical Structure tata_toto (x : toto) X :=
Tata (toto2 x X).
Check fun (T : toto) (t : toto1 T) =>
(eq_refl _ : @tata1 _ = @toto2 _ t).
|
