The following functions can't be defined at Init.Data.List.Basic, because they depend on Init.Util,
and Init.Util depends on Init.Data.List.Basic.
Alternative getters #
get? #
get! #
getD #
Returns the element at the provided index, counting from 0. Returns fallback if the index is out
of bounds.
To return an Option depending on whether the index is in bounds, use as[i]?. To panic if the
index is out of bounds, use as[i]!.
Examples:
getLast! #
Returns the last element in the list. Panics and returns default if the list is empty.
Safer alternatives include:
getLast?, which returns anOption,getLastD, which takes a fallback value for empty lists, andgetLast, which requires a proof that the list is non-empty.
Examples:
Head and tail #
head! #
Returns the first element in the list. If the list is empty, panics and returns default.
Safer alternatives include:
List.head, which requires a proof that the list is non-empty,List.head?, which returns anOption, andList.headD, which returns an explicitly-provided fallback value on empty lists.
tail! #
Drops the first element of a nonempty list, returning the tail. If the list is empty, this function panics when executed and returns the empty list.
Safer alternatives include
tail, which returns the empty list without panicking,tail?, which returns anOption, andtailD, which returns a fallback value when passed the empty list.
Examples:
partitionM #
Returns a pair of lists that together contain all the elements of as. The first list contains
those elements for which the monadic predicate p returns true, and the second contains those for
which p returns false. The list's elements are examined in order, from left to right.
This is a monadic version of List.partition.
Example:
def posOrNeg (x : Int) : Except String Bool :=
if x > 0 then pure true
else if x < 0 then pure false
else throw "Zero is not positive or negative"
#eval [-1, 2, 3].partitionM posOrNeg
Except.ok ([2, 3], [-1])
#eval [0, 2, 3].partitionM posOrNeg
Except.error "Zero is not positive or negative"
Equations
- List.partitionM p l = List.partitionM.go p l #[] #[]
Auxiliary for partitionM:
partitionM.go p l acc₁ acc₂ returns (acc₁.toList ++ left, acc₂.toList ++ right)
if partitionM p l returns (left, right).
partitionMap #
Applies a function that returns a disjoint union to each element of a list, collecting the Sum.inl
and Sum.inr results into separate lists.
Examples:
[0, 1, 2, 3].partitionMap (fun x => if x % 2 = 0 then .inl x else .inr x) = ([0, 2], [1, 3])[0, 1, 2, 3].partitionMap (fun x => if x = 0 then .inl x else .inr x) = ([0], [1, 2, 3])
Equations
- List.partitionMap f l = List.partitionMap.go f l #[] #[]
Auxiliary for partitionMap:
partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)
if partitionMap f l = (left, right).
Equations
- List.partitionMap.go f [] x✝¹ x✝ = (x✝¹.toList, x✝.toList)
- List.partitionMap.go f (x_3 :: xs) x✝¹ x✝ = match f x_3 with | Sum.inl a => List.partitionMap.go f xs (x✝¹.push a) x✝ | Sum.inr b => List.partitionMap.go f xs x✝¹ (x✝.push b)
mapMono #
This is a performance optimization for List.mapM that avoids allocating a new list when the result of each f a is a pointer equal value a.
For verification purposes, List.mapMono = List.map.
Applies a monadic function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.
Applies a function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.
For verification purposes, List.mapMono = List.map.
This tactic, added to the decreasing_trivial toolbox, proves that
sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions
over a nested inductive like inductive T | mk : List T → T.
Equations
- List.tacticSizeOf_list_dec = Lean.ParserDescr.node `List.tacticSizeOf_list_dec 1024 (Lean.ParserDescr.nonReservedSymbol "sizeOf_list_dec" false)