val forall_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a) : Tot bool
let rec forall_aux (#a:Type) (#b:Type) (env:b) (f: b -> a -> Tot bool) (l:list a)
  : Tot bool
  = match l with
    | [] -> true
    | hd::tl -> if f env hd then forall_aux env f tl else false
val forall_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a) : Tot bool
let rec forall_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a) : Tot bool =
match l with
| [] -> true
| hd :: tl -> if f env hd then forall_aux env f tl else false
List.Helpers.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
List.Helpers.fst
Prims.bool Prims.list List.Helpers.forall_aux
module List.Helpers

open FStar.List.Tot

(* Some basic utility functions for closure converting arguments
   to the higher-order combinators in the list library ...
   for use with KaRaMeL extraction *)
let rec filter_aux (#a:Type)
                   (#b:Type)
                   (env:b)
                   (f:(b -> a -> Tot bool))
                   (l: list a)
    : Tot (m:list a{forall x. memP x m ==> f env x}) =
      match l with
      | [] -> []
      | hd::tl -> if f env hd then hd::filter_aux env f tl else filter_aux env f tl

let rec find_aux (#a:Type)
                 (#b:Type)
                 (env:b)
                 (f:(b -> a -> Tot bool))
                 (l:list a)
    : (option (x:a{f env x})) =
      match l with
      | [] -> None #(x:a{f env x}) //These type annotations are only present because it makes bootstrapping go much faster
      | hd::tl -> if f env hd then Some #(x:a{f env x}) hd else find_aux env f tl

let rec choose_aux  (#a:Type)
                    (#b:Type)
                    (#c:Type)
                    (env:c)
                    (f:(c -> a -> Tot (option b)))
                    (l:list a)
    : list b =
      match l with
      | [] -> []
      | hd::tl ->
        match f env hd with
        | Some i -> i :: choose_aux env f tl
        | None -> choose_aux env f tl

let exists_b_aux (#a:Type) (#b:Type) (env:b) (f:b -> a -> Tot bool) (l:list a) =
  Some? (find_aux env f l)

let mem_rev (#a:eqtype) (l:list a) (x:a) = List.Tot.mem x l

let rec forall_aux (#a:Type) (#b:Type) (env:b) (f: b -> a -> Tot bool) (l:list a)
val forall_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a) : Tot bool
env: b -> f: (_: b -> _: a -> Prims.bool) -> l: Prims.list a -> Prims.bool