15 open Hints_declaration
29 (** val foldl_strong_internal :
30 'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
31 'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
32 let rec foldl_strong_internal l h prefix suffix acc =
35 (fun _ -> Util.eq_rect_Type0_r prefix acc (List.append prefix List.Nil))
36 | List.Cons (hd, tl) ->
39 (foldl_strong_internal l h
40 (List.append prefix (List.Cons (hd, List.Nil))) tl
41 (h prefix hd tl __ acc)))) __
43 (** val foldl_strong :
44 'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
45 'a2) -> 'a2 -> 'a2 **)
46 let foldl_strong l h acc =
47 foldl_strong_internal l h List.Nil l acc
49 (** val foldr_strong_internal :
50 'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
51 'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
52 let rec foldr_strong_internal l h prefix suffix acc =
54 | List.Nil -> (fun _ -> acc)
55 | List.Cons (hd, tl) ->
58 (foldr_strong_internal l h
59 (List.append prefix (List.Cons (hd, List.Nil))) tl acc))) __
61 (** val foldr_strong :
62 'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
63 'a2) -> 'a2 -> 'a2 **)
64 let foldr_strong l h acc =
65 foldr_strong_internal l h List.Nil l acc