29 val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
31 val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
33 val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
35 val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
37 val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
39 val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
41 val dAEMONXXX_inv_rect_Type4 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
43 val dAEMONXXX_inv_rect_Type3 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
45 val dAEMONXXX_inv_rect_Type2 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
47 val dAEMONXXX_inv_rect_Type1 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
49 val dAEMONXXX_inv_rect_Type0 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
51 val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __
53 val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __
55 val ltb : Nat.nat -> Nat.nat -> Bool.bool
57 val geb : Nat.nat -> Nat.nat -> Bool.bool
59 val gtb : Nat.nat -> Nat.nat -> Bool.bool
61 val eq_nat : Nat.nat -> Nat.nat -> Bool.bool
63 val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
65 val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list
68 ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list -> 'a1
70 val remove_n_first_internal :
71 Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list
73 val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list
75 val foldi_from_until_internal :
76 Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
77 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list
79 val foldi_from_until :
80 Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) ->
81 'a1 List.list -> 'a1 List.list -> 'a1 List.list
84 Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
85 List.list -> 'a1 List.list -> 'a1 List.list
88 Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
89 List.list -> 'a1 List.list -> 'a1 List.list
92 (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list -> 'a1
93 List.list -> 'a1 List.list
95 val hd_safe : 'a1 List.list -> 'a1
97 val tail_safe : 'a1 List.list -> 'a1 List.list
100 'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod
102 val nth_safe : Nat.nat -> 'a1 List.list -> 'a1
104 val last_safe : 'a1 List.list -> 'a1
107 'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
108 Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
111 'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
112 Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
116 ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
120 ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
123 ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
124 List.list -> 'a4 List.list
126 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
128 val safe_nth : Nat.nat -> 'a1 List.list -> 'a1
130 val nub_by_internal :
131 ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list
133 val nub_by : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
135 val member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool
137 val take : Nat.nat -> 'a1 List.list -> 'a1 List.list
139 val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list
142 Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod
145 Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
147 val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
150 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
153 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
156 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
159 val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
161 val rev : 'a1 List.list -> 'a1 List.list
163 val fold_left_i_aux :
164 (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1
167 (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
169 val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2
171 val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1
173 val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
175 val division : Nat.nat -> Nat.nat -> Nat.nat
177 val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
179 val modulus : Nat.nat -> Nat.nat -> Nat.nat
181 val divide_with_remainder :
182 Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod
184 val less_than_or_equal_b_elim :
185 Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
189 val dpi1__o__bool_to_Prop__o__inject :
190 (Bool.bool, 'a1) Types.dPair -> __ Types.sig0
192 val eject__o__bool_to_Prop__o__inject : Bool.bool Types.sig0 -> __ Types.sig0
194 val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0
196 val dpi1__o__bool_to_Prop_to_eq__o__inject :
197 Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
199 val eject__o__bool_to_Prop_to_eq__o__inject :
200 Bool.bool -> __ Types.sig0 -> __ Types.sig0
202 val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
204 val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
205 Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
207 val eject__o__not_bool_to_Prop_to_eq__o__inject :
208 Bool.bool -> __ Types.sig0 -> __ Types.sig0
210 val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
212 val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
214 val dpi1__o__not_neq_None__o__inject :
215 'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0
217 val eject__o__not_neq_None__o__inject :
218 'a1 Types.option -> __ Types.sig0 -> __ Types.sig0
220 val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0
222 val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
224 val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
226 val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
228 val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2
231 ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
232 Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool
235 ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
236 Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool