val choose_aux (#a #b #c: Type) (env: c) (f: (c -> a -> Tot (option b))) (l: list a) : list b
val choose_aux (#a #b #c: Type) (env: c) (f: (c -> a -> Tot (option b))) (l: list a) : list b
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
module MiTLS.List.Helpers
open MiTLS

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
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
MiTLS.List.Helpers.fst
env: c -> f: (_: c -> _: a -> FStar.Pervasives.Native.option b) -> l: Prims.list a -> Prims.list b
FStar.Pervasives.Native.option Prims.list Prims.Nil Prims.Cons MiTLS.List.Helpers.choose_aux
let rec choose_aux (#a #b #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