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
|
Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.
Definition eq_op (T : eqType) : T -> T -> bool :=
match T with Pack_eq _ op => op end.
Definition bool_eqb b1 b2 :=
match b1, b2 with
| false, false => true
| true, true => true
| _, _ => false
end.
Canonical bool_TYPE := Pack_TYPE bool.
Canonical bool_eqType := Pack_eq bool bool_eqb.
Canonical nat_TYPE := Pack_TYPE nat.
Canonical nat_eqType := Pack_eq nat Nat.eqb.
Definition prod_eqb (T U : eqType) (x y : T * U) :=
match x, y with
| (x1, x2), (y1, y2) =>
andb (eq_op _ x1 y1) (eq_op _ x2 y2)
end.
Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).
Definition sum_eqb (T U : eqType) (x y : T + U) :=
match x, y with
| inl x, inl y => eq_op _ x y
| inr x, inr y => eq_op _ x y
| _, _ => false
end.
Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).
Print Canonical Projections bool.
Print Canonical Projections nat.
Print Canonical Projections prod.
Print Canonical Projections sum.
Print Canonical Projections sort_TYPE.
Print Canonical Projections sort_eq.
Print Canonical Projections sort_TYPE bool.
Print Canonical Projections bool_eqType.
|
