11 type void = unit (* empty inductive *)
13 val void_rect_Type4 : void -> 'a1
15 val void_rect_Type5 : void -> 'a1
17 val void_rect_Type3 : void -> 'a1
19 val void_rect_Type2 : void -> 'a1
21 val void_rect_Type1 : void -> 'a1
23 val void_rect_Type0 : void -> 'a1
28 val unit_rect_Type4 : 'a1 -> unit0 -> 'a1
30 val unit_rect_Type5 : 'a1 -> unit0 -> 'a1
32 val unit_rect_Type3 : 'a1 -> unit0 -> 'a1
34 val unit_rect_Type2 : 'a1 -> unit0 -> 'a1
36 val unit_rect_Type1 : 'a1 -> unit0 -> 'a1
38 val unit_rect_Type0 : 'a1 -> unit0 -> 'a1
40 val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1
42 val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1
44 val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1
46 val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1
48 val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1
50 val unit_discr : unit0 -> unit0 -> __
56 val sum_rect_Type4 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
58 val sum_rect_Type5 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
60 val sum_rect_Type3 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
62 val sum_rect_Type2 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
64 val sum_rect_Type1 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
66 val sum_rect_Type0 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
68 val sum_inv_rect_Type4 :
69 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
71 val sum_inv_rect_Type3 :
72 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
74 val sum_inv_rect_Type2 :
75 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
77 val sum_inv_rect_Type1 :
78 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
80 val sum_inv_rect_Type0 :
81 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
83 val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __
89 val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
91 val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
93 val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
95 val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
97 val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
99 val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
101 val option_inv_rect_Type4 :
102 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
104 val option_inv_rect_Type3 :
105 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
107 val option_inv_rect_Type2 :
108 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
110 val option_inv_rect_Type1 :
111 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
113 val option_inv_rect_Type0 :
114 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
116 val option_discr : 'a1 option -> 'a1 option -> __
118 val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option
120 val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2
122 val refute_none_by_refl :
123 ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3
125 type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
127 val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
129 val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
131 val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
133 val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
135 val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
137 val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
139 val dpi1 : ('a1, 'a2) dPair -> 'a1
141 val dpi2 : ('a1, 'a2) dPair -> 'a2
143 val dPair_inv_rect_Type4 :
144 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
146 val dPair_inv_rect_Type3 :
147 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
149 val dPair_inv_rect_Type2 :
150 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
152 val dPair_inv_rect_Type1 :
153 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
155 val dPair_inv_rect_Type0 :
156 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
158 val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __
162 (* singleton inductive, whose constructor was mk_Sig *)
164 val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
166 val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
168 val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
170 val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
172 val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
174 val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
176 val pi1 : 'a1 sig0 -> 'a1
178 val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
180 val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
182 val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
184 val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
186 val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
188 val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __
190 type ('a, 'b) prod = { fst : 'a; snd : 'b }
192 val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
194 val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
196 val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
198 val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
200 val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
202 val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
204 val fst : ('a1, 'a2) prod -> 'a1
206 val snd : ('a1, 'a2) prod -> 'a2
208 val prod_inv_rect_Type4 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
210 val prod_inv_rect_Type3 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
212 val prod_inv_rect_Type2 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
214 val prod_inv_rect_Type1 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
216 val prod_inv_rect_Type0 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
218 val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __
220 val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod
222 val dpi1__o__coerc_pair_sigma :
223 (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod