29 (** val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
30 let rec all p = function
31 | List.Nil -> Bool.True
32 | List.Cons (h, t) -> Bool.andb (p h) (all p t)
34 (** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
37 | List.Nil -> (fun _ -> List.Nil)
38 | List.Cons (hd, tl) -> (fun _ -> List.Cons ((f hd __), (map_All f tl))))
47 (** val append : 'a1 List.list List.aop **)
51 (** val list : Monad.monadProps **)
53 Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
54 List.foldr (fun x -> List.append (f x)) List.Nil l)
56 (** val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
57 let rec count f = function
59 | List.Cons (x, l') ->
62 | Bool.True -> Nat.S Nat.O
63 | Bool.False -> Nat.O) (count f l')
65 (** val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
66 let position_of_safe test l =
67 Option.opt_safe (List.position_of test l)
69 (** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
71 position_of_safe test l
73 (** val ordered_insert :
74 ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list **)
75 let rec ordered_insert lt a = function
76 | List.Nil -> List.Cons (a, List.Nil)
79 | Bool.True -> List.Cons (a, (List.Cons (h, t)))
80 | Bool.False -> List.Cons (h, (ordered_insert lt a t)))
83 ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
84 let rec insert_sort lt = function
85 | List.Nil -> List.Nil
86 | List.Cons (h, t) -> ordered_insert lt h (insert_sort lt t)
88 (** val range_strong_internal :
89 Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list **)
90 let rec range_strong_internal index how_many end0 =
92 | Nat.O -> (fun _ -> List.Nil)
94 (fun _ -> List.Cons (index,
95 (range_strong_internal (Nat.S index) k end0)))) __
97 (** val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list **)
98 let range_strong end0 =
99 range_strong_internal Nat.O end0 end0