blob: 41322045f2b37f916071f990ed4fcdff0e2f3fed (
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
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 B C D : Type).
Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
Local Coercion ac : A >-> C.
Local Coercion cd : C >-> D.
Local Coercion ab : A >-> B.
Local Coercion bc : B >-> C.
(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *)
(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
Print Graph.
End test2.
End test2.
Module test3.
Section test3.
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 test3.
End test3.
Module test4.
Section test4.
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 test4.
End test4.
Module test5.
Section test5.
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 test5.
End test5.
Module test6.
Record > NAT := wrap_nat { unwrap_nat :> nat }.
Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE := wrap_Type { unwrap_Type :> Type }.
End test6.
Module test7.
Set Primitive Projections.
Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
End test7.
|
