open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Div_and_mod

open Jmeq

open Russell

open Util

(** val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
let rec all p = function
| List.Nil -> Bool.True
| List.Cons (h, t) -> Bool.andb (p h) (all p t)

(** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
let rec map_All f l =
  (match l with
   | List.Nil -> (fun _ -> List.Nil)
   | List.Cons (hd, tl) -> (fun _ -> List.Cons ((f hd __), (map_All f tl))))
    __

open Setoids

open Monad

open Option

(** val append : 'a1 List.list List.aop **)
let append =
  List.append

(** val list : Monad.monadProps **)
let list =
  Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
    List.foldr (fun x -> List.append (f x)) List.Nil l)

(** val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
let rec count f = function
| List.Nil -> Nat.O
| List.Cons (x, l') ->
  Nat.plus
    (match f x with
     | Bool.True -> Nat.S Nat.O
     | Bool.False -> Nat.O) (count f l')

(** val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
let position_of_safe test l =
  Option.opt_safe (List.position_of test l)

(** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
let index_of test l =
  position_of_safe test l

(** val ordered_insert :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list **)
let rec ordered_insert lt a = function
| List.Nil -> List.Cons (a, List.Nil)
| List.Cons (h, t) ->
  (match lt a h with
   | Bool.True -> List.Cons (a, (List.Cons (h, t)))
   | Bool.False -> List.Cons (h, (ordered_insert lt a t)))

(** val insert_sort :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
let rec insert_sort lt = function
| List.Nil -> List.Nil
| List.Cons (h, t) -> ordered_insert lt h (insert_sort lt t)

(** val range_strong_internal :
    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list **)
let rec range_strong_internal index how_many end0 =
  (match how_many with
   | Nat.O -> (fun _ -> List.Nil)
   | Nat.S k ->
     (fun _ -> List.Cons (index,
       (range_strong_internal (Nat.S index) k end0)))) __

(** val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list **)
let range_strong end0 =
  range_strong_internal Nat.O end0 end0