F* stdlib List module.
F* standard library List module.
Base operations *val hd:Unidentified product: [list 'a] (ML 'a)[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 tail:Unidentified product: [list 'a] (ML (list 'a))[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 tl:Unidentified product: [list 'a] (ML (list 'a))[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 last:Unidentified product: [list 'a] (ML 'a)[last l] returns the last element of [l]. Requires, at type-checking time, that [l] be nonempty. Named as in: Haskell
val init:Unidentified product: [list 'a] (ML (list 'a))[init l] returns [l] without its last element. Requires, at type-checking time, that [l] be nonempty. Named as in: Haskell
[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 Iterators *val iter:Unidentified product: [(Unidentified product: ['a] (ML unit))] Unidentified product: [list 'a] (ML unit)[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 iteri_aux:Unidentified product: [int] Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (ML unit))] Unidentified product: [list 'a] (ML unit)[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:Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (ML unit))] Unidentified product: [list 'a] (ML unit)[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 map:Unidentified product: [(Unidentified product: ['a] (ML 'b))] Unidentified product: [list 'a] (ML (list 'b))[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 mapT:Unidentified product: [(Unidentified product: ['a] (Tot 'b))] Unidentified product: [list 'a] (Tot (list 'b))[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 mapi_init:Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (ML 'b))] Unidentified product: [list 'a] Unidentified product: [int] (ML (list 'b))[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:Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (ML 'b))] Unidentified product: [list 'a] (ML (list 'b))[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
[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 map2:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (ML 'c))] Unidentified product: [list 'a] Unidentified product: [list 'b] (ML (list 'c))[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 map3:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] Unidentified product: ['c] (ML 'd))] Unidentified product: [list 'a] Unidentified product: [list 'b] Unidentified product: [list 'c] (ML (list 'd))[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 fold_left:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (ML 'a))] Unidentified product: ['a] Unidentified product: [list 'b] (ML 'a)[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_left2:Unidentified product: [(Unidentified product: ['s] Unidentified product: ['a] Unidentified product: ['b] (ML 's))] Unidentified product: ['s] Unidentified product: [list 'a] Unidentified product: [list 'b] (ML 's)[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_right:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (ML 'b))] Unidentified product: [list 'a] Unidentified product: ['b] (ML 'b)[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
List searching *val filter:Unidentified product: [(Unidentified product: ['a] (ML bool))] Unidentified product: [list 'a] (ML (list 'a))[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 for_all:Unidentified product: [(Unidentified product: ['a] (ML bool))] Unidentified product: [list 'a] (ML bool)[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 forall2:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (ML bool))] Unidentified product: [list 'a] Unidentified product: [list 'b] (ML bool)[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 collect:Unidentified product: [(Unidentified product: ['a] (ML (list 'b)))] Unidentified product: [list 'a] (ML (list 'b))[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 tryFind:Unidentified product: [(Unidentified product: ['a] (ML bool))] Unidentified product: [list 'a] (ML (option 'a))[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 tryPick:Unidentified product: [(Unidentified product: ['a] (ML (option 'b)))] Unidentified product: [list 'a] (ML (option 'b))[tryPick f l] returns [y] for some element [x] appearing in [l] such that [f x = Some y] for some y, or [None] only if [f x = None] for all elements [x] of [l]. (Hides [List.Tot.tryPick], which requires, at type-checking time, [f] to be a pure total function.)
val choose:Unidentified product: [(Unidentified product: ['a] (ML (option 'b)))] Unidentified product: [list 'a] (ML (list 'b))[choose f l] returns the list of [y] for all elements [x] appearing in [l] such that [f x = Some y] for some [y]. (Hides [List.Tot.choose] which requires, at type-checking time, [f] to be a pure total function.)
val partition:Unidentified product: [(Unidentified product: ['a] (ML bool))] Unidentified product: [list 'a] (ML (*(list 'a, list 'a)))[partition f l] returns the pair of lists [(l1, l2)] where all elements [x] of [l] are in [l1] if [f x] holds, and in [l2] otherwise. Both [l1] and [l2] retain the original order of [l]. (Hides [List.Tot.partition], which requires, at type-checking time, [f] to be a pure total function.)
List of tuples *val zip:Unidentified product: [list 'a] Unidentified product: [list 'b] (ML (list (*('a, 'b))))[zip] takes two lists [x1, ..., xn] and [y1, ..., yn] and returns the list of pairs [(x1, y1), ..., (xn, yn)]. Raises an exception if the two lists have different lengths. Named as in: Haskell
Sorting (implemented as quicksort) *val sortWith:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['a] (ML int))] Unidentified product: [list 'a] (ML (list 'a))[sortWith compare l] returns the list [l'] containing the elements of [l] sorted along the comparison function [compare], in such a way that if [compare x y > 0], then [x] appears before [y] in [l']. (Hides [List.Tot.sortWith], which requires, at type-checking time, [compare] to be a pure total function.)
val splitAt:Unidentified product: [nat] Unidentified product: [list 'a] (ML (*(list 'a, list 'a)))[splitAt n l] returns the pair of lists [(l1, l2)] such that [l1] contains the first [n] elements of [l] and [l2] contains the rest. Raises an exception if [l] has fewer than [n] elements.
let ((filter_map (f:Unidentified product: ['a] (ML (option 'b))) (l:list 'a)):(ML (list 'b))):let rec ((filter_map_acc (acc:list 'b) (l:list 'a)):(ML (list 'b)))=match l with [] -> rev acc | (Prims.Cons hd tl) -> match f hd with (Some hd) -> filter_map_acc ((Prims.Cons hd acc)) tl | None -> filter_map_acc acc tl in filter_map_acc (Prims.Nil ) l[filter_map f l] returns the list of [y] for all elements [x] appearing in [l] such that [f x = Some y] for some [y]. (Implemented here as a tail-recursive version of [choose]
val index:Unidentified product: [(Unidentified product: ['a] (ML bool))] Unidentified product: [list 'a] (ML int)[index f l] returns the position index in list [l] of the first element [x] in [l] such that [f x] holds. Raises an exception if no such [x] exists. TODO: rename this function (it hides List.Tot.index which has a completely different semantics.)