21 | Cons of 'a * 'a list
23 (** val list_rect_Type4 :
24 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
25 let rec list_rect_Type4 h_nil h_cons = function
27 | Cons (x_723, x_722) ->
28 h_cons x_723 x_722 (list_rect_Type4 h_nil h_cons x_722)
30 (** val list_rect_Type3 :
31 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
32 let rec list_rect_Type3 h_nil h_cons = function
34 | Cons (x_733, x_732) ->
35 h_cons x_733 x_732 (list_rect_Type3 h_nil h_cons x_732)
37 (** val list_rect_Type2 :
38 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
39 let rec list_rect_Type2 h_nil h_cons = function
41 | Cons (x_738, x_737) ->
42 h_cons x_738 x_737 (list_rect_Type2 h_nil h_cons x_737)
44 (** val list_rect_Type1 :
45 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
46 let rec list_rect_Type1 h_nil h_cons = function
48 | Cons (x_743, x_742) ->
49 h_cons x_743 x_742 (list_rect_Type1 h_nil h_cons x_742)
51 (** val list_rect_Type0 :
52 'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
53 let rec list_rect_Type0 h_nil h_cons = function
55 | Cons (x_748, x_747) ->
56 h_cons x_748 x_747 (list_rect_Type0 h_nil h_cons x_747)
58 (** val list_inv_rect_Type4 :
59 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
61 let list_inv_rect_Type4 hterm h1 h2 =
62 let hcut = list_rect_Type4 h1 h2 hterm in hcut __
64 (** val list_inv_rect_Type3 :
65 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
67 let list_inv_rect_Type3 hterm h1 h2 =
68 let hcut = list_rect_Type3 h1 h2 hterm in hcut __
70 (** val list_inv_rect_Type2 :
71 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
73 let list_inv_rect_Type2 hterm h1 h2 =
74 let hcut = list_rect_Type2 h1 h2 hterm in hcut __
76 (** val list_inv_rect_Type1 :
77 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
79 let list_inv_rect_Type1 hterm h1 h2 =
80 let hcut = list_rect_Type1 h1 h2 hterm in hcut __
82 (** val list_inv_rect_Type0 :
83 'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
85 let list_inv_rect_Type0 hterm h1 h2 =
86 let hcut = list_rect_Type0 h1 h2 hterm in hcut __
88 (** val list_discr : 'a1 list -> 'a1 list -> __ **)
92 | Nil -> Obj.magic (fun _ dH -> dH)
93 | Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
95 (** val append : 'a1 list -> 'a1 list -> 'a1 list **)
96 let rec append l1 l2 =
99 | Cons (hd, tl) -> Cons (hd, (append tl l2))
101 (** val hd : 'a1 list -> 'a1 -> 'a1 **)
107 (** val tail : 'a1 list -> 'a1 list **)
110 | Cons (hd0, tl) -> tl
112 (** val option_hd : 'a1 list -> 'a1 Types.option **)
113 let option_hd = function
115 | Cons (a, x) -> Types.Some a
117 (** val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list **)
118 let option_cons c l =
121 | Types.Some c0 -> Cons (c0, l)
123 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
124 let rec map f = function
126 | Cons (x, tl) -> Cons ((f x), (map f tl))
128 (** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
129 let rec foldr f b = function
131 | Cons (a, l0) -> f a (foldr f b l0)
133 (** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **)
137 | Bool.True -> Cons (x, l0)
138 | Bool.False -> l0) Nil
140 (** val compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
141 let compose f l1 l2 =
142 foldr (fun i acc -> append (map (f i) l2) acc) Nil l1
144 (** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
145 let rec rev_append l1 l2 =
148 | Cons (a, tl) -> rev_append tl (Cons (a, l2))
150 (** val reverse : 'a1 list -> 'a1 list **)
154 (** val length : 'a1 list -> Nat.nat **)
155 let rec length = function
157 | Cons (a, tl) -> Nat.S (length tl)
160 'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
161 let rec split_rev l acc = function
162 | Nat.O -> { Types.fst = acc; Types.snd = l }
165 | Nil -> { Types.fst = acc; Types.snd = Nil }
166 | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)
168 (** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
170 let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
171 { Types.fst = (reverse l1); Types.snd = l2 }
173 (** val flatten : 'a1 list list -> 'a1 list **)
177 (** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
181 | Nat.S m -> nth m (tail l) d
183 (** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
184 let rec nth_opt n = function
188 | Nat.O -> Types.Some h
189 | Nat.S m -> nth_opt m t)
192 ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
194 let rec fold op b p f = function
198 | Bool.True -> op (f a) (fold op b p f l0)
199 | Bool.False -> fold op b p f l0)
203 (* singleton inductive, whose constructor was mk_Aop *)
205 (** val aop_rect_Type4 :
206 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
207 let rec aop_rect_Type4 nil h_mk_Aop x_783 =
208 let op = x_783 in h_mk_Aop op __ __ __
210 (** val aop_rect_Type5 :
211 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
212 let rec aop_rect_Type5 nil h_mk_Aop x_785 =
213 let op = x_785 in h_mk_Aop op __ __ __
215 (** val aop_rect_Type3 :
216 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
217 let rec aop_rect_Type3 nil h_mk_Aop x_787 =
218 let op = x_787 in h_mk_Aop op __ __ __
220 (** val aop_rect_Type2 :
221 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
222 let rec aop_rect_Type2 nil h_mk_Aop x_789 =
223 let op = x_789 in h_mk_Aop op __ __ __
225 (** val aop_rect_Type1 :
226 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
227 let rec aop_rect_Type1 nil h_mk_Aop x_791 =
228 let op = x_791 in h_mk_Aop op __ __ __
230 (** val aop_rect_Type0 :
231 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
232 let rec aop_rect_Type0 nil h_mk_Aop x_793 =
233 let op = x_793 in h_mk_Aop op __ __ __
235 (** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
239 (** val aop_inv_rect_Type4 :
240 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
242 let aop_inv_rect_Type4 x2 hterm h1 =
243 let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
245 (** val aop_inv_rect_Type3 :
246 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
248 let aop_inv_rect_Type3 x2 hterm h1 =
249 let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
251 (** val aop_inv_rect_Type2 :
252 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
254 let aop_inv_rect_Type2 x2 hterm h1 =
255 let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
257 (** val aop_inv_rect_Type1 :
258 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
260 let aop_inv_rect_Type1 x2 hterm h1 =
261 let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
263 (** val aop_inv_rect_Type0 :
264 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
266 let aop_inv_rect_Type0 x2 hterm h1 =
267 let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
269 (** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
270 let aop_discr a2 x y =
271 Logic.eq_rect_Type2 x
272 (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
274 (** val dpi1__o__op :
275 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
276 let dpi1__o__op x1 x3 =
279 (** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
280 let rec lhd l = function
285 | Cons (a, l0) -> Cons (a, (lhd l0 n0)))
287 (** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
288 let rec ltl l = function
290 | Nat.S n0 -> ltl (tail l) n0
292 (** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
293 let rec find f = function
297 | Types.None -> find f t
298 | Types.Some b -> Types.Some b)
300 (** val position_of_aux :
301 ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
302 let rec position_of_aux found l acc =
307 | Bool.True -> Types.Some acc
308 | Bool.False -> position_of_aux found t (Nat.S acc))
310 (** val position_of :
311 ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
312 let position_of found l =
313 position_of_aux found l Nat.O
315 (** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
316 let rec make_list a = function
318 | Nat.S m -> Cons (a, (make_list a m))