val tryFind: ('a -> ML bool) -> list 'a -> ML (option 'a)
let rec tryFind p l = match l with
    | [] -> None
    | hd::tl -> if p hd then Some hd else tryFind p tl
val tryFind: ('a -> ML bool) -> list 'a -> ML (option 'a)
let rec tryFind p l =
match l with
| [] -> None
| hd :: tl -> if p hd then Some hd else tryFind p tl
FStar.List.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.All.fst.checked
FStar.List.fst
Prims.bool Prims.list FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Pervasives.Native.Some FStar.List.tryFind
(*
   Copyright 2008-2014 Nikhil Swamy and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

(**
F* standard library List module. 

@summary F* stdlib List module. 
*)
module FStar.List
open FStar.All
include FStar.List.Tot

(** Base operations **)

(** [hd l] returns the first element of [l]. Raises an exception if
[l] is empty (thus, [hd] hides [List.Tot.hd] which requires [l] to be
nonempty at type-checking time.) Named as in: OCaml, F#, Coq *)
val hd: list 'a -> ML 'a
let hd = function
  | hd::tl -> hd
  | _ -> failwith "head of empty list"

(** [tail l] returns [l] without its first element. Raises an
exception if [l] is empty (thus, [tail] hides [List.Tot.tail] which
requires [l] to be nonempty at type-checking time). Similar to: tl in
OCaml, F#, Coq *)
val tail: list 'a -> ML (list 'a)
let tail = function
  | hd::tl -> tl
  | _ -> failwith "tail of empty list"

(** [tl l] returns [l] without its first element. Raises an exception
if [l] is empty (thus, [tl] hides [List.Tot.tl] which requires [l] to
be nonempty at type-checking time). Named as in: tl in OCaml, F#, Coq
*)
val tl : list 'a -> ML (list 'a)
let tl l = tail l

(** [last l] returns the last element of [l]. Requires, at
type-checking time, that [l] be nonempty. Named as in: Haskell
*)
val last: list 'a -> ML 'a
let rec last = function
  | [hd] -> hd
  | _::tl -> last tl
  | _ -> failwith "last of empty list"

(** [init l] returns [l] without its last element. Requires, at
type-checking time, that [l] be nonempty. Named as in: Haskell
*)
val init: list 'a -> ML (list 'a)
let rec init = function
  | [_] -> []
  | hd::tl -> hd::(init tl)
  | _ -> failwith "init of empty list"

(** [nth l n] returns the [n]-th element in list [l] (with the first
element being the 0-th) if [l] is long enough, or raises an exception
otherwise (thus, [nth] hides [List.Tot.nth] which has [option] type.)
Named as in: OCaml, F#, Coq *)

val nth: list 'a -> int -> ML 'a
let rec nth l n =
  if n < 0 then
    failwith "nth takes a non-negative integer as input"
  else
    if n = 0 then
      match l with
        | [] -> failwith "not enough elements"
        | hd::_ -> hd
    else
      match l with
        | [] -> failwith "not enough elements"
        | _::tl -> nth tl (n - 1)

(** Iterators **)

(** [iter f l] performs [f x] for each element [x] of [l], in the
order in which they appear in [l]. Named as in: OCaml, F# . *)
val iter: ('a -> ML unit) -> list 'a -> ML unit
let rec iter f x = match x with
  | [] -> ()
  | a::tl -> let _ = f a in iter f tl

(** [iteri_aux n f l] performs, for each i, [f (i+n) x] for the i-th
element [x] of [l], in the order in which they appear in [l]. *)
val iteri_aux: int -> (int -> 'a -> ML unit) -> list 'a -> ML unit
let rec iteri_aux i f x = match x with
  | [] -> ()
  | a::tl -> f i a; iteri_aux (i+1) f tl

(** [iteri_aux f l] performs, for each [i], [f i x] for the i-th
element [x] of [l], in the order in which they appear in [l]. Named as
in: OCaml *)
val iteri: (int -> 'a -> ML unit) -> list 'a -> ML unit
let iteri f x = iteri_aux 0 f x

(** [map f l] applies [f] to each element of [l] and returns the list
of results, in the order of the original elements in [l]. (Hides
[List.Tot.map] which requires, at type-checking time, [f] to be a pure
total function.)  Named as in: OCaml, Coq, F# *)
val map: ('a -> ML 'b) -> list 'a -> ML (list 'b)
let rec map f x = match x with
  | [] -> []
  | a::tl -> f a::map f tl

(** [mapT f l] applies [f] to each element of [l] and returns the list
of results, in the order of the original elements in [l]. Requires, at
type-checking time, [f] to be a pure total function. *)
val mapT: ('a -> Tot 'b) -> list 'a -> Tot (list 'b)
let mapT = FStar.List.Tot.map

(** [mapi_init f n l] applies, for each [k], [f (n+k)] to the [k]-th
element of [l] and returns the list of results, in the order of the
original elements in [l]. (Hides [List.Tot.mapi_init] which requires,
at type-checking time, [f] to be a pure total function.) *)
val mapi_init: (int -> 'a -> ML 'b) -> list 'a -> int -> ML (list 'b)
let rec mapi_init f l i = match l with
    | [] -> []
    | hd::tl -> (f i hd)::(mapi_init f tl (i+1))

(** [mapi f l] applies, for each [k], [f k] to the [k]-th element of
[l] and returns the list of results, in the order of the original
elements in [l]. (Hides [List.Tot.mapi] which requires, at
type-checking time, [f] to be a pure total function.) Named as in:
OCaml *)
val mapi: (int -> 'a -> ML 'b) -> list 'a -> ML (list 'b)
let mapi f l = mapi_init f l 0

(** [concatMap f l] applies [f] to each element of [l] and returns the
concatenation of the results, in the order of the original elements of
[l]. This is equivalent to [flatten (map f l)]. (Hides
[List.Tot.concatMap], which requires, at type-checking time, [f] to be
a pure total function.) *)

val concatMap: ('a -> ML (list 'b)) -> list 'a -> ML (list 'b)
let rec concatMap f = function
  | [] -> []
  | a::tl ->
    let fa = f a in
    let ftl = concatMap f tl in
    fa @ ftl

(** [map2 f l1 l2] computes [f x1 x2] for each element x1 of [l1] and
the element [x2] of [l2] at the same position, and returns the list of
such results, in the order of the original elements in [l1]. Raises an
exception if [l1] and [l2] have different lengths.  Named as in: OCaml
*)
val map2: ('a -> 'b -> ML 'c) -> list 'a -> list 'b -> ML (list 'c)
let rec map2 f l1 l2 = match l1, l2 with
    | [], [] -> []
    | hd1::tl1, hd2::tl2 -> (f hd1 hd2)::(map2 f tl1 tl2)
    | _, _ -> failwith "The lists do not have the same length"

(** [map3 f l1 l2 l3] computes [f x1 x2 x3] for each element x1 of
[l1] and the element [x2] of [l2] and the element [x3] of [l3] at the
same position, and returns the list of such results, in the order of
the original elements in [l1]. Raises an exception if [l1], [l2] and
[l3] have different lengths.  Named as in: OCaml *)
val map3: ('a -> 'b -> 'c -> ML 'd) -> list 'a -> list 'b -> list 'c -> ML (list 'd)
let rec map3 f l1 l2 l3 = match l1, l2, l3 with
    | [], [], [] -> []
    | hd1::tl1, hd2::tl2, hd3::tl3 -> (f hd1 hd2 hd3)::(map3 f tl1 tl2 tl3)
    | _, _, _ -> failwith "The lists do not have the same length"

(** [fold_left f x [y1; y2; ...; yn]] computes (f (... (f x y1) y2)
... yn). (Hides [List.Tot.fold_left], which requires, at type-checking
time, [f] to be a pure total function.) Named as in: OCaml, Coq *)
val fold_left: ('a -> 'b -> ML 'a) -> 'a -> list 'b -> ML 'a
let rec fold_left f x y = match y with
  | [] -> x
  | hd::tl -> fold_left f (f x hd) tl

(** [fold_left2 f x [y1; y2; ...; yn] [z1; z2; ...; zn]] computes (f
(... (f x y1 z1) y2 z2 ... yn zn). Raises an exception if [y1; y2;
...] and [z1; z2; ...] have different lengths. (Thus, hides
[List.Tot.fold_left2] which requires such a condition at type-checking
time.) Named as in: OCaml *)
val fold_left2: ('s -> 'a -> 'b -> ML 's) -> 's -> list 'a -> list 'b -> ML 's
let rec fold_left2 f a l1 l2 = match l1, l2 with
    | [], [] -> a
    | hd1::tl1, hd2::tl2 -> fold_left2 f (f a hd1 hd2) tl1 tl2
    | _, _ -> failwith "The lists do not have the same length"

(** [fold_right f [x1; x2; ...; xn] y] computes (f x1 (f x2 (... (f xn
y)) ... )). (Hides [List.Tot.fold_right], which requires, at
type-checking time, [f] to be a pure total function.) Named as in:
OCaml, Coq *)
val fold_right: ('a -> 'b -> ML 'b) -> list 'a -> 'b -> ML 'b
let rec fold_right f l x = match l with
  | [] -> x
  | hd::tl -> f hd (fold_right f tl x)

(** List searching **)

(** [filter f l] returns [l] with all elements [x] such that [f x]
does not hold removed. (Hides [List.Tot.filter] which requires, at
type-checking time, [f] to be a pure total function.) Named as in:
OCaml, Coq *)
val filter: ('a -> ML bool) -> list 'a -> ML (list 'a)
let rec filter f = function
  | [] -> []
  | hd::tl -> if f hd then hd::(filter f tl) else filter f tl

(** [for_all f l] returns [true] if, and only if, for all elements [x]
appearing in [l], [f x] holds. (Hides [List.Tot.for_all], which
requires, at type-checking time, [f] to be a pure total function.)
Named as in: OCaml. Similar to: List.forallb in Coq *)
val for_all: ('a -> ML bool) -> list 'a -> ML bool
let rec for_all f l = match l with
    | [] -> true
    | hd::tl -> if f hd then for_all f tl else false

(** [for_all f l1 l2] returns [true] if, and only if, for all elements
[x1] appearing in [l1] and the element [x2] appearing in [l2] at the
same position, [f x1 x2] holds. Raises an exception if [l1] and [l2]
have different lengths. Similar to: List.for_all2 in OCaml. Similar
to: List.Forall2 in Coq (which is propositional) *)
val forall2: ('a -> 'b -> ML bool) -> list 'a -> list 'b -> ML bool
let rec forall2 f l1 l2 = match l1,l2 with
    | [], [] -> true
    | hd1::tl1, hd2::tl2 -> if f hd1 hd2 then forall2 f tl1 tl2 else false
    | _, _ -> failwith "The lists do not have the same length"

(** [collect f l] applies [f] to each element of [l] and returns the
concatenation of the results, in the order of the original elements of
[l]. It is equivalent to [flatten (map f l)]. (Hides
[List.Tot.collect] which requires, at type-checking time, [f] to be a
pure total function.) TODO: what is the difference with [concatMap]?
*)
val collect: ('a -> ML (list 'b)) -> list 'a -> ML (list 'b)
let rec collect f l = match l with
    | [] -> []
    | hd::tl -> append (f hd) (collect f tl)

(** [tryFind f l] returns [Some x] for some element [x] appearing in
[l] such that [f x] holds, or [None] only if no such [x]
exists. (Hides [List.Tot.tryFind], which requires, at type-checking
time, [f] to be a pure total function.)  *)
val tryFind: ('a -> ML bool) -> list 'a -> ML (option 'a)
p: (_: 'a -> FStar.All.ML Prims.bool) -> l: Prims.list 'a
  -> FStar.All.ML (FStar.Pervasives.Native.option 'a)