blob: a4af27539c42909a3fe260042bbf9942b8dc69ed (
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
Module test1.
Section test1.
Variable (A B C D : Type).
Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D).
Local Coercion ab : A >-> B.
Local Coercion bd : B >-> D.
Local Coercion ac : A >-> C.
Local Coercion cd : C >-> D.
Print Graph.
End test1.
End test1.
Module test2.
Section test2.
Variable (A : Type) (P Q : A -> Prop).
Record B := {
B_A : A;
B_P : P B_A }.
Record C := {
C_A : A;
C_Q : Q C_A }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion B_A : B >-> A.
Local Coercion C_A : C >-> A.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B := Build_B (D_A d) (D_P d).
Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
Print Graph.
End test2.
End test2.
Module test3.
Section test3.
Variable (A : Type) (P Q : A -> Prop).
Definition A' (x : bool) := A.
Record B (x : bool) := {
B_A' : A' x;
B_P : P B_A' }.
Record C (x : bool) := {
C_A' : A' x;
C_Q : Q C_A' }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion A'_A (x : bool) (a : A' x) : A := a.
Local Coercion B_A' : B >-> A'.
Local Coercion C_A' : C >-> A'.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B false := Build_B false (D_A d) (D_P d).
Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
Print Graph.
End test3.
End test3.
Module test4.
Section test4.
Variable (A : Type) (P Q : A -> Prop).
Record A' (x : bool) := { A'_A : A }.
Record B (x : bool) := {
B_A' : A' x;
B_P : P (A'_A x B_A') }.
Record C (x : bool) := {
C_A' : A' x;
C_Q : Q (A'_A x C_A') }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion A'_A : A' >-> A.
Local Coercion B_A' : B >-> A'.
Local Coercion C_A' : C >-> A'.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B false :=
Build_B false (Build_A' false (D_A d)) (D_P d).
Local Coercion D_C (d : D) : C true :=
Build_C true (Build_A' true (D_A d)) (D_Q d).
Print Graph.
End test4.
End test4.
|
