18.15.3.1. Predicates and Relations
🔗defList.IsPrefix.{u} {
α :
Type u} (
l₁ l₂ :
List α) :
PropList.IsPrefix.{u} {
α :
Type u}
(
l₁ l₂ :
List α) :
Prop
The first list is a prefix of the second.
IsPrefix l₁ l₂, written l₁ <+: l₂, means that there exists some t : List α such that l₂ has
the form l₁ ++ t.
The function List.isPrefixOf is a Boolean equivalent.
Conventions for notations in identifiers:
syntaxList Prefix
term ::= ...
| The first list is a prefix of the second.
`IsPrefix l₁ l₂`, written `l₁ <+: l₂`, means that there exists some `t : List α` such that `l₂` has
the form `l₁ ++ t`.
The function `List.isPrefixOf` is a Boolean equivalent.
Conventions for notations in identifiers:
* The recommended spelling of `<+:` in identifiers is `prefix` (not `isPrefix`).
The first list is a prefix of the second.
IsPrefix l₁ l₂, written l₁ <+: l₂, means that there exists some t : List α such that l₂ has
the form l₁ ++ t.
The function List.isPrefixOf is a Boolean equivalent.
Conventions for notations in identifiers:
🔗defList.IsSuffix.{u} {
α :
Type u} (
l₁ l₂ :
List α) :
PropList.IsSuffix.{u} {
α :
Type u}
(
l₁ l₂ :
List α) :
Prop
The first list is a suffix of the second.
IsSuffix l₁ l₂, written l₁ <:+ l₂, means that there exists some t : List α such that l₂ has
the form t ++ l₁.
The function List.isSuffixOf is a Boolean equivalent.
Conventions for notations in identifiers:
syntaxList Suffix
term ::= ...
| The first list is a suffix of the second.
`IsSuffix l₁ l₂`, written `l₁ <:+ l₂`, means that there exists some `t : List α` such that `l₂` has
the form `t ++ l₁`.
The function `List.isSuffixOf` is a Boolean equivalent.
Conventions for notations in identifiers:
* The recommended spelling of `<:+` in identifiers is `suffix` (not `isSuffix`).
The first list is a suffix of the second.
IsSuffix l₁ l₂, written l₁ <:+ l₂, means that there exists some t : List α such that l₂ has
the form t ++ l₁.
The function List.isSuffixOf is a Boolean equivalent.
Conventions for notations in identifiers:
🔗defList.IsInfix.{u} {
α :
Type u} (
l₁ l₂ :
List α) :
PropList.IsInfix.{u} {
α :
Type u}
(
l₁ l₂ :
List α) :
Prop
The first list is a contiguous sub-list of the second list. Typically written with the <:+:
operator.
In other words, l₁ <:+: l₂ means that there exist lists s : List α and t : List α such that
l₂ has the form s ++ l₁ ++ t.
Conventions for notations in identifiers:
syntaxList Infix
term ::= ...
| The first list is a contiguous sub-list of the second list. Typically written with the `<:+:`
operator.
In other words, `l₁ <:+: l₂` means that there exist lists `s : List α` and `t : List α` such that
`l₂` has the form `s ++ l₁ ++ t`.
Conventions for notations in identifiers:
* The recommended spelling of `<:+:` in identifiers is `infix` (not `isInfix`).
The first list is a contiguous sub-list of the second list. Typically written with the <:+:
operator.
In other words, l₁ <:+: l₂ means that there exist lists s : List α and t : List α such that
l₂ has the form s ++ l₁ ++ t.
Conventions for notations in identifiers:
🔗inductive predicateList.Sublist.{u_1} {
α :
Type u_1} :
List α →
List α →
PropList.Sublist.{u_1} {
α :
Type u_1} :
List α →
List α →
Prop
The first list is a non-contiguous sub-list of the second list. Typically written with the <+
operator.
In other words, l₁ <+ l₂ means that l₁ can be transformed into l₂ by repeatedly inserting new
elements.
Constructors
slnil.{u_1} {α : Type u_1} : [].Sublist []
The base case: [] is a sublist of []
cons.{u_1} {α : Type u_1} {l₁ l₂ : List α} (a : α) :
l₁.Sublist l₂ → l₁.Sublist (a :: l₂)
If l₁ is a subsequence of l₂, then it is also a subsequence of a :: l₂.
cons₂.{u_1} {α : Type u_1} {l₁ l₂ : List α} (a : α) :
l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)
If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: l₂.
syntaxSublists
term ::= ...
| The first list is a non-contiguous sub-list of the second list. Typically written with the `<+`
operator.
In other words, `l₁ <+ l₂` means that `l₁` can be transformed into `l₂` by repeatedly inserting new
elements.
The first list is a non-contiguous sub-list of the second list. Typically written with the <+
operator.
In other words, l₁ <+ l₂ means that l₁ can be transformed into l₂ by repeatedly inserting new
elements.
This syntax is only available when the List namespace is opened.
🔗inductive predicateList.Perm.{u} {
α :
Type u} :
List α →
List α →
PropList.Perm.{u} {
α :
Type u} :
List α →
List α →
Prop
Two lists are permutations of each other if they contain the same elements, each occurring the same
number of times but not necessarily in the same order.
One list can be proven to be a permutation of another by showing how to transform one into the other
by repeatedly swapping adjacent elements.
List.isPerm is a Boolean equivalent of this relation.
Constructors
nil.{u} {α : Type u} : [].Perm []
The empty list is a permutation of the empty list: [] ~ [].
cons.{u} {α : Type u} (x : α) {l₁ l₂ : List α} :
l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)
If one list is a permutation of the other, adding the same element as the head of each yields
lists that are permutations of each other: l₁ ~ l₂ → x::l₁ ~ x::l₂.
swap.{u} {α : Type u} (x y : α) (l : List α) :
(y :: x :: l).Perm (x :: y :: l)
If two lists are identical except for having their first two elements swapped, then they are
permutations of each other: x::y::l ~ y::x::l.
trans.{u} {α : Type u} {l₁ l₂ l₃ : List α} :
l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃
Permutation is transitive: l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃.
syntaxList Permutation
term ::= ...
| Two lists are permutations of each other if they contain the same elements, each occurring the same
number of times but not necessarily in the same order.
One list can be proven to be a permutation of another by showing how to transform one into the other
by repeatedly swapping adjacent elements.
`List.isPerm` is a Boolean equivalent of this relation.
Two lists are permutations of each other if they contain the same elements, each occurring the same
number of times but not necessarily in the same order.
One list can be proven to be a permutation of another by showing how to transform one into the other
by repeatedly swapping adjacent elements.
List.isPerm is a Boolean equivalent of this relation.
This syntax is only available when the List namespace is opened.
🔗inductive predicateList.Pairwise.{u} {
α :
Type u} (
R :
α →
α →
Prop) :
List α →
PropList.Pairwise.{u} {
α :
Type u}
(
R :
α →
α →
Prop) :
List α →
Prop
Each element of a list is related to all later elements of the list by R.
Pairwise R l means that all the elements of l with earlier indexes are R-related to all the
elements with later indexes.
For example, Pairwise (· ≠ ·) l asserts that l has no duplicates, and if Pairwise (· < ·) l
asserts that l is (strictly) sorted.
Examples:
-
Pairwise (· < ·) [1, 2, 3] ↔ (1 < 2 ∧ 1 < 3) ∧ 2 < 3
-
Pairwise (· = ·) [1, 2, 3] = False
-
Pairwise (· ≠ ·) [1, 2, 3] = True
Constructors
nil.{u} {α : Type u} {R : α → α → Prop} : List.Pairwise R []
All elements of the empty list are vacuously pairwise related.
cons.{u} {α : Type u} {R : α → α → Prop} {a : α}
{l : List α} :
(∀ (a' : α), a' ∈ l → R a a') →
List.Pairwise R l → List.Pairwise R (a :: l)
A nonempty list is pairwise related with R if the head is related to every element of the tail
and the tail is itself pairwise related.
That is, a :: l is Pairwise R if:
🔗defList.Nodup.{u} {
α :
Type u} :
List α →
PropList.Nodup.{u} {
α :
Type u} :
List α →
Prop
The list has no duplicates: it contains every element at most once.
It is defined as Pairwise (· ≠ ·): each element is unequal to all other elements.
🔗inductive predicateList.Lex.{u} {
α :
Type u} (
r :
α →
α →
Prop) (
as bs :
List α) :
PropList.Lex.{u} {
α :
Type u}
(
r :
α →
α →
Prop) (
as bs :
List α) :
Prop
Lexicographic ordering for lists with respect to an ordering of elements.
as is lexicographically smaller than bs if
-
as is empty and bs is non-empty, or
-
both as and bs are non-empty, and the head of as is less than the head of bs according to
r, or
-
both as and bs are non-empty, their heads are equal, and the tail of as is less than the
tail of bs.
Constructors
nil.{u} {α : Type u} {r : α → α → Prop} {a : α}
{l : List α} : List.Lex r [] (a :: l)
[] is the smallest element in the lexicographic order.
rel.{u} {α : Type u} {r : α → α → Prop} {a₁ : α}
{l₁ : List α} {a₂ : α} {l₂ : List α} (h : r a₁ a₂) :
List.Lex r (a₁ :: l₁) (a₂ :: l₂)
If the head of the first list is smaller than the head of the second, then the first list is
lexicographically smaller than the second list.
cons.{u} {α : Type u} {r : α → α → Prop} {a : α}
{l₁ l₂ : List α} (h : List.Lex r l₁ l₂) :
List.Lex r (a :: l₁) (a :: l₂)
If two lists have the same head, then their tails determine their lexicographic order. If the tail
of the first list is lexicographically smaller than the tail of the second list, then the entire
first list is lexicographically smaller than the entire second list.
🔗inductive predicateList.Mem.{u} {
α :
Type u} (
a :
α) :
List α →
PropList.Mem.{u} {
α :
Type u} (
a :
α) :
List α →
Prop
List membership, typically accessed via the ∈ operator.
a ∈ l means that a is an element of the list l. Elements are compared according to Lean's
logical equality.
The related function List.elem is a Boolean membership test that uses a BEq α instance.
Examples:
Constructors
head.{u} {α : Type u} {a : α} (as : List α) :
List.Mem a (a :: as)
The head of a list is a member: a ∈ a :: as.
tail.{u} {α : Type u} {a : α} (b : α) {as : List α} :
List.Mem a as → List.Mem a (b :: as)
A member of the tail of a list is a member of the list: a ∈ l → a ∈ b :: l.
18.15.3.2. Constructing Lists
🔗defList.singleton.{u} {
α :
Type u} (
a :
α) :
List αList.singleton.{u} {
α :
Type u} (
a :
α) :
List α
Constructs a single-element list.
Examples:
🔗defList.concat.{u} {
α :
Type u} :
List α →
α →
List αList.concat.{u} {
α :
Type u} :
List α →
α →
List α
Adds an element to the end of a list.
The added element is the last element of the resulting list.
Examples:
🔗defList.replicate.{u} {
α :
Type u} (
n :
Nat) (
a :
α) :
List αList.replicate.{u} {
α :
Type u} (
n :
Nat)
(
a :
α) :
List α
Creates a list that contains n copies of a.
🔗defList.replicateTR.{u} {
α :
Type u} (
n :
Nat) (
a :
α) :
List αList.replicateTR.{u} {
α :
Type u}
(
n :
Nat) (
a :
α) :
List α
Creates a list that contains n copies of a.
This is a tail-recursive version of List.replicate.
🔗defList.ofFn.{u_1} {
α :
Type u_1} {
n :
Nat} (
f :
Fin n →
α) :
List αList.ofFn.{u_1} {
α :
Type u_1} {
n :
Nat}
(
f :
Fin n →
α) :
List α
Creates a list by applying f to each potential index in order, starting at 0.
Examples:
-
List.ofFn (n := 3) toString = ["0", "1", "2"]
-
List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]
🔗defList.append.{u} {
α :
Type u} (
xs ys :
List α) :
List αList.append.{u} {
α :
Type u}
(
xs ys :
List α) :
List α
Appends two lists. Normally used via the ++ operator.
Appending lists takes time proportional to the length of the first list: O(|xs|).
Examples:
-
[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5].
-
[] ++ [4, 5] = [4, 5].
-
[1, 2, 3] ++ [] = [1, 2, 3].
🔗defList.appendTR.{u} {
α :
Type u} (
as bs :
List α) :
List αList.appendTR.{u} {
α :
Type u}
(
as bs :
List α) :
List α
Appends two lists. Normally used via the ++ operator.
Appending lists takes time proportional to the length of the first list: O(|xs|).
This is a tail-recursive version of List.append.
Examples:
-
[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5].
-
[] ++ [4, 5] = [4, 5].
-
[1, 2, 3] ++ [] = [1, 2, 3].
🔗def
Returns a list of the numbers from 0 to n exclusive, in increasing order.
O(n).
Examples:
-
range 5 = [0, 1, 2, 3, 4]
-
range 0 = []
-
range 2 = [0, 1]
🔗def
Returns a list of the numbers with the given length len, starting at start and increasing by
step at each element.
In other words, List.range' start len step is [start, start+step, ..., start+(len-1)*step].
Examples:
-
List.range' 0 3 (step := 1) = [0, 1, 2]
-
List.range' 0 3 (step := 2) = [0, 2, 4]
-
List.range' 0 4 (step := 2) = [0, 2, 4, 6]
-
List.range' 3 4 (step := 2) = [3, 5, 7, 9]
🔗def
Returns a list of the numbers with the given length len, starting at start and increasing by
step at each element.
In other words, List.range'TR start len step is [start, start+step, ..., start+(len-1)*step].
This is a tail-recursive version of List.range'.
Examples:
-
List.range'TR 0 3 (step := 1) = [0, 1, 2]
-
List.range'TR 0 3 (step := 2) = [0, 2, 4]
-
List.range'TR 0 4 (step := 2) = [0, 2, 4, 6]
-
List.range'TR 3 4 (step := 2) = [3, 5, 7, 9]
🔗def
Lists all elements of Fin n in order, starting at 0.
Examples:
18.15.3.5. Lookups
🔗def
Returns the element at the provided index, counting from 0.
In other words, for i : Fin as.length, as.get i returns the i'th element of the list as.
Because the index is a Fin bounded by the list's length, the index will never be out of bounds.
Examples:
-
["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"
-
["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"
🔗defList.getD.{u_1} {
α :
Type u_1} (
as :
List α) (
i :
Nat) (
fallback :
α) :
αList.getD.{u_1} {
α :
Type u_1}
(
as :
List α) (
i :
Nat) (
fallback :
α) :
α
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:
-
["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"
-
["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"
-
["spring", "summer", "fall", "winter"].getD 4 "never" = "never"
🔗defList.getLast.{u} {
α :
Type u} (
as :
List α) :
as ≠ [] →
αList.getLast.{u} {
α :
Type u}
(
as :
List α) :
as ≠ [] →
α
Returns the last element of a non-empty list.
Examples:
🔗defList.getLast?.{u} {
α :
Type u} :
List α →
Option αList.getLast?.{u} {
α :
Type u} :
List α →
Option α
Returns the last element in the list, or none if the list is empty.
Alternatives include List.getLastD, which takes a fallback value for empty lists, and
List.getLast!, which panics on empty lists.
Examples:
🔗defList.getLastD.{u} {
α :
Type u} (
as :
List α) (
fallback :
α) :
αList.getLastD.{u} {
α :
Type u}
(
as :
List α) (
fallback :
α) :
α
Returns the last element in the list, or fallback if the list is empty.
Alternatives include List.getLast?, which returns an Option, and List.getLast!, which panics
on empty lists.
Examples:
🔗def
Returns the last element in the list. Panics and returns default if the list is empty.
Safer alternatives include:
-
getLast?, which returns an Option,
-
getLastD, which takes a fallback value for empty lists, and
-
getLast, which requires a proof that the list is non-empty.
Examples:
🔗defList.lookup.{u, v} {
α :
Type u} {
β :
Type v} [
BEq α] :
α →
List (α × β) →
Option βList.lookup.{u, v} {
α :
Type u}
{
β :
Type v} [
BEq α] :
α →
List (α × β) →
Option β
Treats the list as an association list that maps keys to values, returning the first value whose key
is equal to the specified key.
O(|l|).
Examples:
-
[(1, "one"), (3, "three"), (3, "other")].lookup 3 = some "three"
-
[(1, "one"), (3, "three"), (3, "other")].lookup 2 = none
🔗def
Returns the largest element of the list if it is not empty, or none if it is empty.
Examples:
🔗def
Returns the smallest element of the list if it is not empty, or none if it is empty.
Examples:
18.15.3.6. Queries
🔗defList.count.{u} {
α :
Type u} [
BEq α] (
a :
α) :
List α →
NatList.count.{u} {
α :
Type u} [
BEq α]
(
a :
α) :
List α →
Nat
Counts the number of times an element occurs in a list.
Examples:
-
[1, 1, 2, 3, 5].count 1 = 2
-
[1, 1, 2, 3, 5].count 5 = 1
-
[1, 1, 2, 3, 5].count 4 = 0
🔗defList.countP.{u} {
α :
Type u} (
p :
α →
Bool) (
l :
List α) :
NatList.countP.{u} {
α :
Type u}
(
p :
α →
Bool) (
l :
List α) :
Nat
Counts the number of elements in the list l that satisfy the Boolean predicate p.
Examples:
-
[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2
-
[1, 2, 3, 4, 5].countP (· < 5) = 4
-
[1, 2, 3, 4, 5].countP (· > 5) = 0
🔗defList.idxOf.{u} {
α :
Type u} [
BEq α] (
a :
α) :
List α →
NatList.idxOf.{u} {
α :
Type u} [
BEq α]
(
a :
α) :
List α →
Nat
Returns the index of the first element equal to a, or the length of the list if no element is
equal to a.
Examples:
-
["carrot", "potato", "broccoli"].idxOf "carrot" = 0
-
["carrot", "potato", "broccoli"].idxOf "broccoli" = 2
-
["carrot", "potato", "broccoli"].idxOf "tomato" = 3
-
["carrot", "potato", "broccoli"].idxOf "anything else" = 3
🔗def
Returns the index of the first element equal to a, or none if no element is equal to a.
Examples:
-
["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0
-
["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2
-
["carrot", "potato", "broccoli"].idxOf? "tomato" = none
-
["carrot", "potato", "broccoli"].idxOf? "anything else" = none
🔗def
Returns the index of the first element equal to a, or the length of the list if no element is
equal to a. The index is returned as a Fin, which guarantees that it is in bounds.
Examples:
🔗def
Returns the first element of the list for which the predicate p returns true, or none if no
such element is found.
O(|l|).
Examples:
-
[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1
-
[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none
🔗def
Returns the index of the first element for which p returns true, or none if there is no such
element. The index is returned as a Fin, which guarantees that it is in bounds.
Examples:
-
[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)
-
[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none
🔗defList.findIdx.{u} {
α :
Type u} (
p :
α →
Bool) (
l :
List α) :
NatList.findIdx.{u} {
α :
Type u}
(
p :
α →
Bool) (
l :
List α) :
Nat
Returns the index of the first element for which p returns true, or the length of the list if
there is no such element.
Examples:
-
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4
-
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7
🔗def
Returns the index of the first element for which p returns true, or none if there is no such
element.
Examples:
-
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4
-
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none
🔗defList.findM?.{u} {
m :
Type →
Type u} [
Monad m] {
α :
Type}
(
p :
α →
m Bool) :
List α →
m (
Option α)
List.findM?.{u} {
m :
Type →
Type u}
[
Monad m] {
α :
Type} (
p :
α →
m Bool) :
List α →
m (
Option α)
Returns the first element of the list for which the monadic predicate p returns true, or none
if no such element is found. Elements of the list are checked in order.
O(|l|).
Example:
some 1Almost! 6
Almost! 5
#eval [7, 6, 5, 8, 1, 2, 6].findM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
Almost! 6
Almost! 5some 1
🔗defList.findSome?.{u, v} {
α :
Type u} {
β :
Type v} (
f :
α →
Option β) :
List α →
Option βList.findSome?.{u, v} {
α :
Type u}
{
β :
Type v} (
f :
α →
Option β) :
List α →
Option β
Returns the first non-none result of applying f to each element of the list in order. Returns
none if f returns none for all elements of the list.
O(|l|).
Examples:
-
[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
-
[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none
🔗defList.findSomeM?.{u, v, w} {
m :
Type u →
Type v} [
Monad m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m (
Option β)) :
List α →
m (
Option β)
List.findSomeM?.{u, v, w}
{
m :
Type u →
Type v} [
Monad m]
{
α :
Type w} {
β :
Type u}
(
f :
α →
m (
Option β)) :
List α →
m (
Option β)
Returns the first non-none result of applying the monadic function f to each element of the
list, in order. Returns none if f returns none for all elements.
O(|l|).
Example:
some 10Almost! 6
Almost! 5
#eval [7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
Almost! 6
Almost! 5some 10
18.15.3.8. Modification
🔗defList.set.{u_1} {
α :
Type u_1} (
l :
List α) (
n :
Nat) (
a :
α) :
List αList.set.{u_1} {
α :
Type u_1} (
l :
List α)
(
n :
Nat) (
a :
α) :
List α
Replaces the value at (zero-based) index n in l with a. If the index is out of bounds, then
the list is returned unmodified.
Examples:
-
["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]
-
["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]
🔗defList.setTR.{u_1} {
α :
Type u_1} (
l :
List α) (
n :
Nat) (
a :
α) :
List αList.setTR.{u_1} {
α :
Type u_1}
(
l :
List α) (
n :
Nat) (
a :
α) :
List α
Replaces the value at (zero-based) index n in l with a. If the index is out of bounds, then
the list is returned unmodified.
This is a tail-recursive version of List.set that's used at runtime.
Examples:
-
["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]
-
["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]
🔗defList.modify.{u} {
α :
Type u} (
l :
List α) (
i :
Nat) (
f :
α →
α) :
List αList.modify.{u} {
α :
Type u} (
l :
List α)
(
i :
Nat) (
f :
α →
α) :
List α
Replaces the element at the given index, if it exists, with the result of applying f to it. If the
index is invalid, the list is returned unmodified.
Examples:
-
[1, 2, 3].modify 0 (· * 10) = [10, 2, 3]
-
[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]
-
[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]
🔗defList.modifyTR.{u_1} {
α :
Type u_1} (
l :
List α) (
i :
Nat) (
f :
α →
α) :
List αList.modifyTR.{u_1} {
α :
Type u_1}
(
l :
List α) (
i :
Nat) (
f :
α →
α) :
List α
Replaces the element at the given index, if it exists, with the result of applying f to it.
This is a tail-recursive version of List.modify.
Examples:
-
[1, 2, 3].modifyTR 0 (· * 10) = [10, 2, 3]
-
[1, 2, 3].modifyTR 2 (· * 10) = [1, 2, 30]
-
[1, 2, 3].modifyTR 3 (· * 10) = [1, 2, 3]
🔗defList.modifyHead.{u} {
α :
Type u} (
f :
α →
α) :
List α →
List αList.modifyHead.{u} {
α :
Type u}
(
f :
α →
α) :
List α →
List α
Replace the head of the list with the result of applying f to it. Returns the empty list if the
list is empty.
Examples:
🔗def
Replaces the nth tail of l with the result of applying f to it. Returns the input without
using f if the index is larger than the length of the List.
Examples:
["circle", "square", "triangle"].modifyTailIdx 1 List.reverse["circle", "triangle", "square"]["circle", "square", "triangle"].modifyTailIdx 1 (fun xs => xs ++ xs)["circle", "square", "triangle", "square", "triangle"]["circle", "square", "triangle"].modifyTailIdx 2 (fun xs => xs ++ xs)["circle", "square", "triangle", "triangle"]["circle", "square", "triangle"].modifyTailIdx 5 (fun xs => xs ++ xs)["circle", "square", "triangle"]
🔗defList.erase.{u_1} {
α :
Type u_1} [
BEq α] :
List α →
α →
List αList.erase.{u_1} {
α :
Type u_1} [
BEq α] :
List α →
α →
List α
Removes the first occurrence of a from l. If a does not occur in l, the list is returned
unmodified.
O(|l|).
Examples:
-
[1, 5, 3, 2, 5].erase 5 = [1, 3, 2, 5]
-
[1, 5, 3, 2, 5].erase 6 = [1, 5, 3, 2, 5]
🔗defList.eraseTR.{u_1} {
α :
Type u_1} [
BEq α] (
l :
List α) (
a :
α) :
List αList.eraseTR.{u_1} {
α :
Type u_1} [
BEq α]
(
l :
List α) (
a :
α) :
List α
Removes the first occurrence of a from l. If a does not occur in l, the list is returned
unmodified.
O(|l|).
This is a tail-recursive version of List.erase, used in runtime code.
Examples:
-
[1, 5, 3, 2, 5].eraseTR 5 = [1, 3, 2, 5]
-
[1, 5, 3, 2, 5].eraseTR 6 = [1, 5, 3, 2, 5]
🔗defList.eraseDups.{u_1} {
α :
Type u_1} [
BEq α] (
as :
List α) :
List αList.eraseDups.{u_1} {
α :
Type u_1}
[
BEq α] (
as :
List α) :
List α
Erases duplicated elements in the list, keeping the first occurrence of duplicated elements.
O(|l|^2).
Examples:
-
[1, 3, 2, 2, 3, 5].eraseDups = [1, 3, 2, 5]
-
["red", "green", "green", "blue"].eraseDups = ["red", "green", "blue"]
🔗defList.eraseIdx.{u} {
α :
Type u} (
l :
List α) (
i :
Nat) :
List αList.eraseIdx.{u} {
α :
Type u}
(
l :
List α) (
i :
Nat) :
List α
Removes the element at the specified index. If the index is out of bounds, the list is returned
unmodified.
O(i).
Examples:
-
[0, 1, 2, 3, 4].eraseIdx 0 = [1, 2, 3, 4]
-
[0, 1, 2, 3, 4].eraseIdx 1 = [0, 2, 3, 4]
-
[0, 1, 2, 3, 4].eraseIdx 5 = [0, 1, 2, 3, 4]
🔗defList.eraseIdxTR.{u_1} {
α :
Type u_1} (
l :
List α) (
n :
Nat) :
List αList.eraseIdxTR.{u_1} {
α :
Type u_1}
(
l :
List α) (
n :
Nat) :
List α
Removes the element at the specified index. If the index is out of bounds, the list is returned
unmodified.
O(i).
This is a tail-recursive version of List.eraseIdx, used at runtime.
Examples:
-
[0, 1, 2, 3, 4].eraseIdxTR 0 = [1, 2, 3, 4]
-
[0, 1, 2, 3, 4].eraseIdxTR 1 = [0, 2, 3, 4]
-
[0, 1, 2, 3, 4].eraseIdxTR 5 = [0, 1, 2, 3, 4]
🔗defList.eraseP.{u} {
α :
Type u} (
p :
α →
Bool) :
List α →
List αList.eraseP.{u} {
α :
Type u}
(
p :
α →
Bool) :
List α →
List α
Removes the first element of a list for which p returns true. If no element satisfies p, then
the list is returned unchanged.
Examples:
-
[2, 1, 2, 1, 3, 4].eraseP (· < 2) = [2, 2, 1, 3, 4]
-
[2, 1, 2, 1, 3, 4].eraseP (· > 2) = [2, 1, 2, 1, 4]
-
[2, 1, 2, 1, 3, 4].eraseP (· > 8) = [2, 1, 2, 1, 3, 4]
🔗defList.erasePTR.{u_1} {
α :
Type u_1} (
p :
α →
Bool) (
l :
List α) :
List αList.erasePTR.{u_1} {
α :
Type u_1}
(
p :
α →
Bool) (
l :
List α) :
List α
Removes the first element of a list for which p returns true. If no element satisfies p, then
the list is returned unchanged.
This is a tail-recursive version of eraseP, used at runtime.
Examples:
-
[2, 1, 2, 1, 3, 4].erasePTR (· < 2) = [2, 2, 1, 3, 4]
-
[2, 1, 2, 1, 3, 4].erasePTR (· > 2) = [2, 1, 2, 1, 4]
-
[2, 1, 2, 1, 3, 4].erasePTR (· > 8) = [2, 1, 2, 1, 3, 4]
🔗defList.eraseReps.{u_1} {
α :
Type u_1} [
BEq α] :
List α →
List αList.eraseReps.{u_1} {
α :
Type u_1}
[
BEq α] :
List α →
List α
Erases repeated elements, keeping the first element of each run.
O(|l|).
Example:
-
[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = [1, 3, 2, 3, 5]
🔗defList.removeAll.{u} {
α :
Type u} [
BEq α] (
xs ys :
List α) :
List αList.removeAll.{u} {
α :
Type u} [
BEq α]
(
xs ys :
List α) :
List α
Removes all elements of xs that are present in ys.
O(|xs| * |ys|).
Examples:
-
[1, 1, 5, 1, 2, 4, 5].removeAll [1, 2, 2] = [5, 4, 5]
-
[1, 2, 3, 2].removeAll [] = [1, 2, 3, 2]
-
[1, 2, 3, 2].removeAll [3] = [1, 2, 2]
🔗defList.replace.{u} {
α :
Type u} [
BEq α] (
l :
List α) (
a b :
α) :
List αList.replace.{u} {
α :
Type u} [
BEq α]
(
l :
List α) (
a b :
α) :
List α
Replaces the first element of the list l that is equal to a with b. If no element is equal to
a, then the list is returned unchanged.
O(|l|).
Examples:
-
[1, 4, 2, 3, 3, 7].replace 3 6 = [1, 4, 2, 6, 3, 7]
-
[1, 4, 2, 3, 3, 7].replace 5 6 = [1, 4, 2, 3, 3, 7]
🔗defList.replaceTR.{u_1} {
α :
Type u_1} [
BEq α] (
l :
List α) (
b c :
α) :
List αList.replaceTR.{u_1} {
α :
Type u_1}
[
BEq α] (
l :
List α) (
b c :
α) :
List α
Replaces the first element of the list l that is equal to a with b. If no element is equal to
a, then the list is returned unchanged.
O(|l|). This is a tail-recursive version of List.replace that's used in runtime code.
Examples:
-
[1, 4, 2, 3, 3, 7].replaceTR 3 6 = [1, 4, 2, 6, 3, 7]
-
[1, 4, 2, 3, 3, 7].replaceTR 5 6 = [1, 4, 2, 3, 3, 7]
🔗defList.reverse.{u} {
α :
Type u} (
as :
List α) :
List αList.reverse.{u} {
α :
Type u}
(
as :
List α) :
List α
Reverses a list.
O(|as|).
Because of the “functional but in place” optimization implemented by Lean's compiler, this function
does not allocate a new list when its reference to the input list is unshared: it simply walks the
linked list and reverses all the node pointers.
Examples:
🔗def
Concatenates a list of lists into a single list, preserving the order of the elements.
O(|flatten L|).
Examples:
-
[["a"], ["b", "c"]].flatten = ["a", "b", "c"]
-
[["a"], [], ["b", "c"], ["d", "e", "f"]].flatten = ["a", "b", "c", "d", "e", "f"]
🔗defList.flattenTR.{u_1} {
α :
Type u_1} (
l :
List (
List α)) :
List αList.flattenTR.{u_1} {
α :
Type u_1}
(
l :
List (
List α)) :
List α
Concatenates a list of lists into a single list, preserving the order of the elements.
O(|flatten L|). This is a tail-recursive version of List.flatten, used in runtime code.
Examples:
-
[["a"], ["b", "c"]].flattenTR = ["a", "b", "c"]
-
[["a"], [], ["b", "c"], ["d", "e", "f"]].flattenTR = ["a", "b", "c", "d", "e", "f"]
🔗defList.rotateLeft.{u} {
α :
Type u} (
xs :
List α) (
i :
Nat := 1) :
List αList.rotateLeft.{u} {
α :
Type u}
(
xs :
List α) (
i :
Nat := 1) :
List α
Rotates the elements of xs to the left, moving i % xs.length elements from the start of the list
to the end.
O(|xs|).
Examples:
-
[1, 2, 3, 4, 5].rotateLeft 3 = [4, 5, 1, 2, 3]
-
[1, 2, 3, 4, 5].rotateLeft 5 = [1, 2, 3, 4, 5]
-
[1, 2, 3, 4, 5].rotateLeft 1 = [2, 3, 4, 5, 1]
🔗defList.rotateRight.{u} {
α :
Type u} (
xs :
List α) (
i :
Nat := 1) :
List αList.rotateRight.{u} {
α :
Type u}
(
xs :
List α) (
i :
Nat := 1) :
List α
Rotates the elements of xs to the right, moving i % xs.length elements from the end of the list
to the start.
After rotation, the element at xs[n] is at index (i + n) % l.length. O(|xs|).
Examples:
-
[1, 2, 3, 4, 5].rotateRight 3 = [3, 4, 5, 1, 2]
-
[1, 2, 3, 4, 5].rotateRight 5 = [1, 2, 3, 4, 5]
-
[1, 2, 3, 4, 5].rotateRight 1 = [5, 1, 2, 3, 4]
🔗defList.leftpad.{u} {
α :
Type u} (
n :
Nat) (
a :
α) (
l :
List α) :
List αList.leftpad.{u} {
α :
Type u} (
n :
Nat)
(
a :
α) (
l :
List α) :
List α
Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l
already has at least n elements, it is returned unmodified.
Examples:
-
[1, 2, 3].leftpad 5 0 = [0, 0, 1, 2, 3]
-
["red", "green", "blue"].leftpad 4 "blank" = ["blank", "red", "green", "blue"]
-
["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]
-
["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]
🔗defList.leftpadTR.{u} {
α :
Type u} (
n :
Nat) (
a :
α) (
l :
List α) :
List αList.leftpadTR.{u} {
α :
Type u} (
n :
Nat)
(
a :
α) (
l :
List α) :
List α
Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l
already has at least n elements, it is returned unmodified.
This is a tail-recursive version of List.leftpad, used at runtime.
Examples:
-
[1, 2, 3].leftPadTR 5 0 = [0, 0, 1, 2, 3]
-
["red", "green", "blue"].leftPadTR 4 "blank" = ["blank", "red", "green", "blue"]
-
["red", "green", "blue"].leftPadTR 3 "blank" = ["red", "green", "blue"]
-
["red", "green", "blue"].leftPadTR 1 "blank" = ["red", "green", "blue"]
🔗defList.rightpad.{u} {
α :
Type u} (
n :
Nat) (
a :
α) (
l :
List α) :
List αList.rightpad.{u} {
α :
Type u} (
n :
Nat)
(
a :
α) (
l :
List α) :
List α
Pads l : List α on the right with repeated occurrences of a : α until it is of length n. If
l already has at least n elements, it is returned unmodified.
Examples:
-
[1, 2, 3].rightpad 5 0 = [1, 2, 3, 0, 0]
-
["red", "green", "blue"].rightpad 4 "blank" = ["red", "green", "blue", "blank"]
-
["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]
-
["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]
18.15.3.8.1. Insertion
🔗defList.insert.{u} {
α :
Type u} [
BEq α] (
a :
α) (
l :
List α) :
List αList.insert.{u} {
α :
Type u} [
BEq α]
(
a :
α) (
l :
List α) :
List α
Inserts an element into a list without duplication.
If the element is present in the list, the list is returned unmodified. Otherwise, the new element
is inserted at the head of the list.
Examples:
-
[1, 2, 3].insert 0 = [0, 1, 2, 3]
-
[1, 2, 3].insert 4 = [4, 1, 2, 3]
-
[1, 2, 3].insert 2 = [1, 2, 3]
🔗defList.insertIdx.{u} {
α :
Type u} (
xs :
List α) (
i :
Nat) (
a :
α) :
List αList.insertIdx.{u} {
α :
Type u}
(
xs :
List α) (
i :
Nat) (
a :
α) :
List α
Inserts an element into a list at the specified index. If the index is greater than the length of
the list, then the list is returned unmodified.
In other words, the new element is inserted into the list l after the first i elements of l.
Examples:
-
["tues", "thur", "sat"].insertIdx 1 "wed" = ["tues", "wed", "thur", "sat"]
-
["tues", "thur", "sat"].insertIdx 2 "wed" = ["tues", "thur", "wed", "sat"]
-
["tues", "thur", "sat"].insertIdx 3 "wed" = ["tues", "thur", "sat", "wed"]
-
["tues", "thur", "sat"].insertIdx 4 "wed" = ["tues", "thur", "sat"]
🔗defList.insertIdxTR.{u_1} {
α :
Type u_1} (
l :
List α) (
n :
Nat) (
a :
α) :
List αList.insertIdxTR.{u_1} {
α :
Type u_1}
(
l :
List α) (
n :
Nat) (
a :
α) :
List α
Inserts an element into a list at the specified index. If the index is greater than the length of
the list, then the list is returned unmodified.
In other words, the new element is inserted into the list l after the first i elements of l.
This is a tail-recursive version of List.insertIdx, used at runtime.
Examples:
-
["tues", "thur", "sat"].insertIdxTR 1 "wed" = ["tues", "wed", "thur", "sat"]
-
["tues", "thur", "sat"].insertIdxTR 2 "wed" = ["tues", "thur", "wed", "sat"]
-
["tues", "thur", "sat"].insertIdxTR 3 "wed" = ["tues", "thur", "sat", "wed"]
-
["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]
🔗defList.intersperse.{u} {
α :
Type u} (
sep :
α) (
l :
List α) :
List αList.intersperse.{u} {
α :
Type u}
(
sep :
α) (
l :
List α) :
List α
Alternates the elements of l with sep.
O(|l|).
List.intercalate is a similar function that alternates a separator list with elements of a list of
lists.
Examples:
🔗defList.intersperseTR.{u} {
α :
Type u} (
sep :
α) (
l :
List α) :
List αList.intersperseTR.{u} {
α :
Type u}
(
sep :
α) (
l :
List α) :
List α
Alternates the elements of l with sep.
O(|l|).
This is a tail-recursive version of List.intersperse, used at runtime.
Examples:
🔗def
Alternates the lists in xs with the separator sep, appending them. The resulting list is
flattened.
O(|xs|).
List.intersperse is a similar function that alternates a separator element with the elements of a
list.
Examples:
🔗defList.intercalateTR.{u_1} {
α :
Type u_1} (
sep :
List α)
(
xs :
List (
List α)) :
List αList.intercalateTR.{u_1} {
α :
Type u_1}
(
sep :
List α) (
xs :
List (
List α)) :
List α
Alternates the lists in xs with the separator sep.
This is a tail-recursive version of List.intercalate used at runtime.
Examples:
🔗defList.map.{u, v} {
α :
Type u} {
β :
Type v} (
f :
α →
β) (
l :
List α) :
List βList.map.{u, v} {
α :
Type u} {
β :
Type v}
(
f :
α →
β) (
l :
List α) :
List β
Applies a function to each element of the list, returning the resulting list of values.
O(|l|).
Examples:
-
[a, b, c].map f = [f a, f b, f c]
-
[].map Nat.succ = []
-
["one", "two", "three"].map (·.length) = [3, 3, 5]
-
["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]
🔗defList.mapTR.{u, v} {
α :
Type u} {
β :
Type v} (
f :
α →
β) (
as :
List α) :
List βList.mapTR.{u, v} {
α :
Type u}
{
β :
Type v} (
f :
α →
β) (
as :
List α) :
List β
Applies a function to each element of the list, returning the resulting list of values.
O(|l|). This is the tail-recursive variant of List.map, used in runtime code.
Examples:
-
[a, b, c].mapTR f = [f a, f b, f c]
-
[].mapTR Nat.succ = []
-
["one", "two", "three"].mapTR (·.length) = [3, 3, 5]
-
["one", "two", "three"].mapTR (·.reverse) = ["eno", "owt", "eerht"]
🔗defList.mapM.{u, v, w} {
m :
Type u →
Type v} [
Monad m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m β) (
as :
List α) :
m (
List β)
List.mapM.{u, v, w} {
m :
Type u →
Type v}
[
Monad m] {
α :
Type w} {
β :
Type u}
(
f :
α →
m β) (
as :
List α) :
m (
List β)
Applies the monadic action f to every element in the list, left-to-right, and returns the list of
results.
This implementation is tail recursive. List.mapM' is a a non-tail-recursive variant that may be
more convenient to reason about. List.forM is the variant that discards the results and
List.mapA is the variant that works with Applicative.
🔗defList.mapM'.{u_1, u_2, u_3} {
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m] (
f :
α →
m β) :
List α →
m (
List β)
List.mapM'.{u_1, u_2, u_3}
{
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m] (
f :
α →
m β) :
List α →
m (
List β)
Applies the monadic action f on every element in the list, left-to-right, and returns the list of
results.
This is a non-tail-recursive variant of List.mapM that's easier to reason about. It cannot be used
as the main definition and replaced by the tail-recursive version because they can only be proved
equal when m is a LawfulMonad.
🔗defList.mapA.{u, v, w} {
m :
Type u →
Type v} [
Applicative m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m β) :
List α →
m (
List β)
List.mapA.{u, v, w} {
m :
Type u →
Type v}
[
Applicative m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m β) :
List α →
m (
List β)
Applies the applicative action f on every element in the list, left-to-right, and returns the list
of results.
If m is also a Monad, then using mapM can be more efficient.
See List.forA for the variant that discards the results. See List.mapM for the variant that
works with Monad.
This function is not tail-recursive, so it may fail with a stack overflow on long lists.
🔗defList.mapFinIdx.{u_1, u_2} {
α :
Type u_1} {
β :
Type u_2} (
as :
List α)
(
f : (
i :
Nat) →
α →
i < as.
length →
β) :
List βList.mapFinIdx.{u_1, u_2} {
α :
Type u_1}
{
β :
Type u_2} (
as :
List α)
(
f :
(
i :
Nat) →
α →
i < as.
length →
β) :
List β
Applies a function to each element of the list along with the index at which that element is found,
returning the list of results. In addition to the index, the function is also provided with a proof
that the index is valid.
List.mapIdx is a variant that does not provide the function with evidence that the index is valid.
🔗defList.mapFinIdxM.{u_1, u_2, u_3} {
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m] (
as :
List α)
(
f : (
i :
Nat) →
α →
i < as.
length →
m β) :
m (
List β)
List.mapFinIdxM.{u_1, u_2, u_3}
{
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m] (
as :
List α)
(
f :
(
i :
Nat) →
α →
i < as.
length →
m β) :
m (
List β)
Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results. In addition to the index, the function is also provided with a
proof that the index is valid.
List.mapIdxM is a variant that does not provide the function with evidence that the index is
valid.
🔗defList.mapIdx.{u_1, u_2} {
α :
Type u_1} {
β :
Type u_2} (
f :
Nat →
α →
β)
(
as :
List α) :
List βList.mapIdx.{u_1, u_2} {
α :
Type u_1}
{
β :
Type u_2} (
f :
Nat →
α →
β)
(
as :
List α) :
List β
Applies a function to each element of the list along with the index at which that element is found,
returning the list of results.
List.mapFinIdx is a variant that additionally provides the function with a proof that the index
is valid.
🔗defList.mapIdxM.{u_1, u_2, u_3} {
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m] (
f :
Nat →
α →
m β) (
as :
List α) :
m (
List β)
List.mapIdxM.{u_1, u_2, u_3}
{
m :
Type u_1 →
Type u_2} {
α :
Type u_3}
{
β :
Type u_1} [
Monad m]
(
f :
Nat →
α →
m β) (
as :
List α) :
m (
List β)
Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results.
List.mapFinIdxM is a variant that additionally provides the function with a proof that the index
is valid.
🔗defList.mapMono.{u_1} {
α :
Type u_1} (
as :
List α) (
f :
α →
α) :
List αList.mapMono.{u_1} {
α :
Type u_1}
(
as :
List α) (
f :
α →
α) :
List α
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.
🔗defList.mapMonoM.{u_1, u_2} {
m :
Type u_1 →
Type u_2} {
α :
Type u_1}
[
Monad m] (
as :
List α) (
f :
α →
m α) :
m (
List α)
List.mapMonoM.{u_1, u_2}
{
m :
Type u_1 →
Type u_2} {
α :
Type u_1}
[
Monad m] (
as :
List α) (
f :
α →
m α) :
m (
List α)
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.
🔗defList.flatMap.{u, v} {
α :
Type u} {
β :
Type v} (
b :
α →
List β)
(
as :
List α) :
List βList.flatMap.{u, v} {
α :
Type u}
{
β :
Type v} (
b :
α →
List β)
(
as :
List α) :
List β
Applies a function that returns a list to each element of a list, and concatenates the resulting
lists.
Examples:
-
[2, 3, 2].flatMap List.range = [0, 1, 0, 1, 2, 0, 1]
-
["red", "blue"].flatMap String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']
🔗defList.flatMapTR.{u_1, u_2} {
α :
Type u_1} {
β :
Type u_2} (
f :
α →
List β)
(
as :
List α) :
List βList.flatMapTR.{u_1, u_2} {
α :
Type u_1}
{
β :
Type u_2} (
f :
α →
List β)
(
as :
List α) :
List β
Applies a function that returns a list to each element of a list, and concatenates the resulting
lists.
This is the tail-recursive version of List.flatMap that's used at runtime.
Examples:
-
[2, 3, 2].flatMapTR List.range = [0, 1, 0, 1, 2, 0, 1]
-
["red", "blue"].flatMapTR String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']
🔗defList.flatMapM.{u, v, w} {
m :
Type u →
Type v} [
Monad m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m (
List β)) (
as :
List α) :
m (
List β)
List.flatMapM.{u, v, w}
{
m :
Type u →
Type v} [
Monad m]
{
α :
Type w} {
β :
Type u}
(
f :
α →
m (
List β)) (
as :
List α) :
m (
List β)
Applies a monadic function that returns a list to each element of a list, from left to right, and
concatenates the resulting lists.
🔗def
Combines two lists into a list of pairs in which the first and second components are the
corresponding elements of each list. The resulting list is the length of the shorter of the input
lists.
O(min |xs| |ys|).
Examples:
-
["Mon", "Tue", "Wed"].zip [1, 2, 3] = [("Mon", 1), ("Tue", 2), ("Wed", 3)]
-
["Mon", "Tue", "Wed"].zip [1, 2] = [("Mon", 1), ("Tue", 2)]
-
[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]
🔗def
Pairs each element of a list with its index, optionally starting from an index other than 0.
O(|l|).
Examples:
-
[a, b, c].zipIdx = [(a, 0), (b, 1), (c, 2)]
-
[a, b, c].zipIdx 5 = [(a, 5), (b, 6), (c, 7)]
🔗def
Pairs each element of a list with its index, optionally starting from an index other than 0.
O(|l|). This is a tail-recursive version of List.zipIdx that's used at runtime.
Examples:
-
[a, b, c].zipIdxTR = [(a, 0), (b, 1), (c, 2)]
-
[a, b, c].zipIdxTR 5 = [(a, 5), (b, 6), (c, 7)]
🔗defList.zipWith.{u, v, w} {
α :
Type u} {
β :
Type v} {
γ :
Type w}
(
f :
α →
β →
γ) (
xs :
List α) (
ys :
List β) :
List γList.zipWith.{u, v, w} {
α :
Type u}
{
β :
Type v} {
γ :
Type w}
(
f :
α →
β →
γ) (
xs :
List α)
(
ys :
List β) :
List γ
Applies a function to the corresponding elements of two lists, stopping at the end of the shorter
list.
O(min |xs| |ys|).
Examples:
-
[1, 2].zipWith (· + ·) [5, 6] = [6, 8]
-
[1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13]
-
[].zipWith (· + ·) [5, 6] = []
-
[x₁, x₂, x₃].zipWith f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
🔗defList.zipWithTR.{u_1, u_2, u_3} {
α :
Type u_1} {
β :
Type u_2}
{
γ :
Type u_3} (
f :
α →
β →
γ) (
as :
List α) (
bs :
List β) :
List γList.zipWithTR.{u_1, u_2, u_3}
{
α :
Type u_1} {
β :
Type u_2}
{
γ :
Type u_3} (
f :
α →
β →
γ)
(
as :
List α) (
bs :
List β) :
List γ
Applies a function to the corresponding elements of two lists, stopping at the end of the shorter
list.
O(min |xs| |ys|). This is a tail-recursive version of List.zipWith that's used at runtime.
Examples:
-
[1, 2].zipWithTR (· + ·) [5, 6] = [6, 8]
-
[1, 2, 3].zipWithTR (· + ·) [5, 6, 10] = [6, 8, 13]
-
[].zipWithTR (· + ·) [5, 6] = []
-
[x₁, x₂, x₃].zipWithTR f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
🔗defList.zipWithAll.{u, v, w} {
α :
Type u} {
β :
Type v} {
γ :
Type w}
(
f :
Option α →
Option β →
γ) :
List α →
List β →
List γList.zipWithAll.{u, v, w} {
α :
Type u}
{
β :
Type v} {
γ :
Type w}
(
f :
Option α →
Option β →
γ) :
List α →
List β →
List γ
Applies a function to the corresponding elements of both lists, stopping when there are no more
elements in either list. If one list is shorter than the other, the function is passed none for
the missing elements.
Examples:
-
[1, 6].zipWithAll min [5, 2] = [some 1, some 2]
-
[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]
-
[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]
🔗defList.unzip.{u, v} {
α :
Type u} {
β :
Type v} (
l :
List (α × β)) :
List α × List βList.unzip.{u, v} {
α :
Type u}
{
β :
Type v} (
l :
List (α × β)) :
List α × List β
Separates a list of pairs into two lists that contain the respective first and second components.
O(|l|).
Examples:
-
[("Monday", 1), ("Tuesday", 2)].unzip = (["Monday", "Tuesday"], [1, 2])
-
[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = ([x₁, x₂, x₃], [y₁, y₂, y₃])
-
([] : List (Nat × String)).unzip = (([], []) : List Nat × List String)
🔗defList.unzipTR.{u, v} {
α :
Type u} {
β :
Type v} (
l :
List (α × β)) :
List α × List βList.unzipTR.{u, v} {
α :
Type u}
{
β :
Type v} (
l :
List (α × β)) :
List α × List β
Separates a list of pairs into two lists that contain the respective first and second components.
O(|l|). This is a tail-recursive version of List.unzip that's used at runtime.
Examples:
-
[("Monday", 1), ("Tuesday", 2)].unzipTR = (["Monday", "Tuesday"], [1, 2])
-
[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzipTR = ([x₁, x₂, x₃], [y₁, y₂, y₃])
-
([] : List (Nat × String)).unzipTR = (([], []) : List Nat × List String)
18.15.3.12. Filtering
🔗defList.filter.{u} {
α :
Type u} (
p :
α →
Bool) (
l :
List α) :
List αList.filter.{u} {
α :
Type u}
(
p :
α →
Bool) (
l :
List α) :
List α
Returns the list of elements in l for which p returns true.
O(|l|).
Examples:
-
[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]
-
[1, 2, 5, 2, 7, 7].filter (fun _ => false) = []
-
[1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 7, 7]
🔗defList.filterTR.{u} {
α :
Type u} (
p :
α →
Bool) (
as :
List α) :
List αList.filterTR.{u} {
α :
Type u}
(
p :
α →
Bool) (
as :
List α) :
List α
Returns the list of elements in l for which p returns true.
O(|l|). This is a tail-recursive version of List.filter, used at runtime.
Examples:
-
[1, 2, 5, 2, 7, 7].filterTR (· > 2) = [5, 7, 7]
-
[1, 2, 5, 2, 7, 7].filterTR (fun _ => false) = []
-
[1, 2, 5, 2, 7, 7].filterTR (fun _ => true) = * [1, 2, 5, 2, 7, 7]
🔗defList.filterM.{v} {
m :
Type →
Type v} [
Monad m] {
α :
Type}
(
p :
α →
m Bool) (
as :
List α) :
m (
List α)
List.filterM.{v} {
m :
Type →
Type v}
[
Monad m] {
α :
Type} (
p :
α →
m Bool)
(
as :
List α) :
m (
List α)
Applies the monadic predicate p to every element in the list, in order from left to right, and
returns the list of elements for which p returns true.
O(|l|).
Example:
[1, 2, 2]Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7
#eval [1, 2, 5, 2, 7, 7].filterM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7[1, 2, 2]
🔗defList.filterRevM.{v} {
m :
Type →
Type v} [
Monad m] {
α :
Type}
(
p :
α →
m Bool) (
as :
List α) :
m (
List α)
List.filterRevM.{v} {
m :
Type →
Type v}
[
Monad m] {
α :
Type} (
p :
α →
m Bool)
(
as :
List α) :
m (
List α)
Applies the monadic predicate p on every element in the list in reverse order, from right to left,
and returns those elements for which p returns true. The elements of the returned list are in
the same order as in the input list.
Example:
[1, 2, 2]Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1
#eval [1, 2, 5, 2, 7, 7].filterRevM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1[1, 2, 2]
🔗defList.filterMap.{u, v} {
α :
Type u} {
β :
Type v} (
f :
α →
Option β) :
List α →
List βList.filterMap.{u, v} {
α :
Type u}
{
β :
Type v} (
f :
α →
Option β) :
List α →
List β
Applies a function that returns an Option to each element of a list, collecting the non-none
values.
O(|l|).
Example:
[10, 14, 14]#eval [1, 2, 5, 2, 7, 7].filterMap fun x =>
if x > 2 then some (2 * x) else none
[10, 14, 14]
🔗defList.filterMapTR.{u_1, u_2} {
α :
Type u_1} {
β :
Type u_2}
(
f :
α →
Option β) (
l :
List α) :
List βList.filterMapTR.{u_1, u_2} {
α :
Type u_1}
{
β :
Type u_2} (
f :
α →
Option β)
(
l :
List α) :
List β
Applies a function that returns an Option to each element of a list, collecting the non-none
values.
O(|l|). This is a tail-recursive version of List.filterMap, used at runtime.
Example:
[10, 14, 14]#eval [1, 2, 5, 2, 7, 7].filterMapTR fun x =>
if x > 2 then some (2 * x) else none
[10, 14, 14]
🔗defList.filterMapM.{u, v, w} {
m :
Type u →
Type v} [
Monad m] {
α :
Type w}
{
β :
Type u} (
f :
α →
m (
Option β)) (
as :
List α) :
m (
List β)
List.filterMapM.{u, v, w}
{
m :
Type u →
Type v} [
Monad m]
{
α :
Type w} {
β :
Type u}
(
f :
α →
m (
Option β)) (
as :
List α) :
m (
List β)
Applies a monadic function that returns an Option to each element of a list, collecting the
non-none values.
O(|l|).
Example:
[10, 14, 14]Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7
#eval [1, 2, 5, 2, 7, 7].filterMapM fun x => do
IO.println s!"Examining {x}"
if x > 2 then return some (2 * x)
else return none
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7[10, 14, 14]
18.15.3.12.1. Partitioning
🔗defList.take.{u} {
α :
Type u} (
n :
Nat) (
xs :
List α) :
List αList.take.{u} {
α :
Type u} (
n :
Nat)
(
xs :
List α) :
List α
Extracts the first n elements of xs, or the whole list if n is greater than xs.length.
O(min n |xs|).
Examples:
-
[a, b, c, d, e].take 0 = []
-
[a, b, c, d, e].take 3 = [a, b, c]
-
[a, b, c, d, e].take 6 = [a, b, c, d, e]
🔗defList.takeTR.{u_1} {
α :
Type u_1} (
n :
Nat) (
l :
List α) :
List αList.takeTR.{u_1} {
α :
Type u_1} (
n :
Nat)
(
l :
List α) :
List α
Extracts the first n elements of xs, or the whole list if n is greater than xs.length.
O(min n |xs|). This is a tail-recursive version of List.take, used at runtime.
Examples:
-
[a, b, c, d, e].takeTR 0 = []
-
[a, b, c, d, e].takeTR 3 = [a, b, c]
-
[a, b, c, d, e].takeTR 6 = [a, b, c, d, e]
🔗defList.takeWhile.{u} {
α :
Type u} (
p :
α →
Bool) (
xs :
List α) :
List αList.takeWhile.{u} {
α :
Type u}
(
p :
α →
Bool) (
xs :
List α) :
List α
Returns the longest initial segment of xs for which p returns true.
O(|xs|).
Examples:
-
[7, 6, 4, 8].takeWhile (· > 5) = [7, 6]
-
[7, 6, 6, 5].takeWhile (· > 5) = [7, 6, 6]
-
[7, 6, 6, 8].takeWhile (· > 5) = [7, 6, 6, 8]
🔗defList.takeWhileTR.{u_1} {
α :
Type u_1} (
p :
α →
Bool) (
l :
List α) :
List αList.takeWhileTR.{u_1} {
α :
Type u_1}
(
p :
α →
Bool) (
l :
List α) :
List α
Returns the longest initial segment of xs for which p returns true.
O(|xs|). This is a tail-recursive version of List.take, used at runtime.
Examples:
-
[7, 6, 4, 8].takeWhileTR (· > 5) = [7, 6]
-
[7, 6, 6, 5].takeWhileTR (· > 5) = [7, 6, 6]
-
[7, 6, 6, 8].takeWhileTR (· > 5) = [7, 6, 6, 8]
🔗defList.drop.{u} {
α :
Type u} (
n :
Nat) (
xs :
List α) :
List αList.drop.{u} {
α :
Type u} (
n :
Nat)
(
xs :
List α) :
List α
Removes the first n elements of the list xs. Returns the empty list if n is greater than the
length of the list.
O(min n |xs|).
Examples:
-
[0, 1, 2, 3, 4].drop 0 = [0, 1, 2, 3, 4]
-
[0, 1, 2, 3, 4].drop 3 = [3, 4]
-
[0, 1, 2, 3, 4].drop 6 = []
🔗defList.dropWhile.{u} {
α :
Type u} (
p :
α →
Bool) :
List α →
List αList.dropWhile.{u} {
α :
Type u}
(
p :
α →
Bool) :
List α →
List α
Removes the longest prefix of a list for which p returns true.
Elements are removed from the list until one is encountered for which p returns false. This
element and the remainder of the list are returned.
O(|l|).
Examples:
-
[1, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [4, 2, 7, 4]
-
[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]
-
[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []
🔗defList.dropLast.{u_1} {
α :
Type u_1} :
List α →
List αList.dropLast.{u_1} {
α :
Type u_1} :
List α →
List α
Removes the last element of the list, if one exists.
Examples:
🔗defList.dropLastTR.{u_1} {
α :
Type u_1} (
l :
List α) :
List αList.dropLastTR.{u_1} {
α :
Type u_1}
(
l :
List α) :
List α
Removes the last element of the list, if one exists.
This is a tail-recursive version of List.dropLast, used at runtime.
Examples:
🔗def
Splits a list at an index, resulting in the first n elements of l paired with the remaining
elements.
If n is greater than the length of l, then the resulting pair consists of l and the empty
list. List.splitAt is equivalent to a combination of List.take and List.drop, but it is more
efficient.
Examples:
-
["red", "green", "blue"].splitAt 2 = (["red", "green"], ["blue"])
-
["red", "green", "blue"].splitAt 3 = (["red", "green", "blue], [])
-
["red", "green", "blue"].splitAt 4 = (["red", "green", "blue], [])
🔗def
Splits a list into the the longest initial segment for which p returns true, paired with the
remainder of the list.
O(|l|).
Examples:
-
[6, 8, 9, 5, 2, 9].span (· > 5) = ([6, 8, 9], [5, 2, 9])
-
[6, 8, 9, 5, 2, 9].span (· > 10) = ([], [6, 8, 9, 5, 2, 9])
-
[6, 8, 9, 5, 2, 9].span (· > 0) = ([6, 8, 9, 5, 2, 9], [])
🔗def
Splits a list into the longest segments in which each pair of adjacent elements are related by R.
O(|l|).
Examples:
-
[1, 1, 2, 2, 2, 3, 2].splitBy (· == ·) = [[1, 1], [2, 2, 2], [3], [2]]
-
[1, 2, 5, 4, 5, 1, 4].splitBy (· < ·) = [[1, 2, 5], [4, 5], [1, 4]]
-
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => true) = [[1, 2, 5, 4, 5, 1, 4]]
-
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => false) = [[1], [2], [5], [4], [5], [1], [4]]
🔗def
Returns a pair of lists that together contain all the elements of as. The first list contains
those elements for which p returns true, and the second contains those for which p returns
false.
O(|l|). as.partition p is equivalent to (as.filter p, as.filter (not ∘ p)), but it is slightly
more efficient since it only has to do one pass over the list.
Examples:
-
[1, 2, 5, 2, 7, 7].partition (· > 2) = ([5, 7, 7], [1, 2, 2])
-
[1, 2, 5, 2, 7, 7].partition (fun _ => false) = ([], [1, 2, 5, 2, 7, 7])
-
[1, 2, 5, 2, 7, 7].partition (fun _ => true) = ([1, 2, 5, 2, 7, 7], [])
🔗def
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"
🔗defList.partitionMap.{u_1, u_2, u_3} {
α :
Type u_1} {
β :
Type u_2}
{
γ :
Type u_3} (
f :
α →
β ⊕ γ) (
l :
List α) :
List β × List γList.partitionMap.{u_1, u_2, u_3}
{
α :
Type u_1} {
β :
Type u_2}
{
γ :
Type u_3} (
f :
α →
β ⊕ γ)
(
l :
List α) :
List β × List γ
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])
🔗defList.groupByKey.{u, v} {
α :
Type u} {
β :
Type v} [
BEq α] [
Hashable α]
(
key :
β →
α) (
xs :
List β) :
Std.HashMap α (
List β)
List.groupByKey.{u, v} {
α :
Type u}
{
β :
Type v} [
BEq α] [
Hashable α]
(
key :
β →
α) (
xs :
List β) :
Std.HashMap α (
List β)
Groups the elements of a list xs according to the function key, returning a hash map in which
each group is associated with its key. Groups preserve the relative order of elements in xs.
Example:
Std.HashMap.ofList [(0, [0, 2, 4, 6]), (1, [1, 3, 5])]#eval [0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
Std.HashMap.ofList [(0, [0, 2, 4, 6]), (1, [1, 3, 5])]
18.15.3.14. Comparisons
🔗def
Checks whether two lists have the same length and their elements are pairwise BEq. Normally used
via the == operator.
🔗defList.isEqv.{u} {
α :
Type u} (
as bs :
List α) (
eqv :
α →
α →
Bool) :
BoolList.isEqv.{u} {
α :
Type u}
(
as bs :
List α) (
eqv :
α →
α →
Bool) :
Bool
Returns true if as and bs have the same length and they are pairwise related by eqv.
O(min |as| |bs|). Short-circuits at the first non-related pair of elements.
Examples:
-
[1, 2, 3].isEqv [2, 3, 4] (· < ·) = true
-
[1, 2, 3].isEqv [2, 2, 4] (· < ·) = false
-
[1, 2, 3].isEqv [2, 3] (· < ·) = false
🔗def
Returns true if l₁ and l₂ are permutations of each other. O(|l₁| * |l₂|).
The relation List.Perm is a logical characterization of permutations. When the BEq α instance
corresponds to DecidableEq α, isPerm l₁ l₂ ↔ l₁ ~ l₂ (use the theorem isPerm_iff).
🔗def
Checks whether the first list is a prefix of the second.
The relation List.IsPrefixOf expresses this property with respect to logical equality.
Examples:
-
[1, 2].isPrefixOf [1, 2, 3] = true
-
[1, 2].isPrefixOf [1, 2] = true
-
[1, 2].isPrefixOf [1] = false
-
[1, 2].isPrefixOf [1, 1, 2, 3] = false
🔗def
If the first list is a prefix of the second, returns the result of dropping the prefix.
In other words, isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.
Examples:
-
[1, 2].isPrefixOf? [1, 2, 3] = some [3]
-
[1, 2].isPrefixOf? [1, 2] = some []
-
[1, 2].isPrefixOf? [1] = none
-
[1, 2].isPrefixOf? [1, 1, 2, 3] = none
🔗def
True if the first list is a potentially non-contiguous sub-sequence of the second list, comparing
elements with the == operator.
The relation List.Sublist is a logical characterization of this property.
Examples:
🔗defList.isSuffixOf.{u} {
α :
Type u} [
BEq α] (
l₁ l₂ :
List α) :
BoolList.isSuffixOf.{u} {
α :
Type u} [
BEq α]
(
l₁ l₂ :
List α) :
Bool
Checks whether the first list is a suffix of the second.
The relation List.IsSuffixOf expresses this property with respect to logical equality.
Examples:
-
[2, 3].isSuffixOf [1, 2, 3] = true
-
[2, 3].isSuffixOf [1, 2, 3, 4] = false
-
[2, 3].isSuffixOf [1, 2] = false
-
[2, 3].isSuffixOf [1, 1, 2, 3] = true
🔗def
If the first list is a suffix of the second, returns the result of dropping the suffix from the
second.
In other words, isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.
Examples:
-
[2, 3].isSuffixOf? [1, 2, 3] = some [1]
-
[2, 3].isSuffixOf? [1, 2, 3, 4] = none
-
[2, 3].isSuffixOf? [1, 2] = none
-
[2, 3].isSuffixOf? [1, 1, 2, 3] = some [1, 1]
🔗defList.le.{u} {
α :
Type u} [
LT α] (
as bs :
List α) :
PropList.le.{u} {
α :
Type u} [
LT α]
(
as bs :
List α) :
Prop
Non-strict ordering of lists with respect to a strict ordering of their elements.
as ≤ bs if ¬ bs < as.
This relation can be treated as a lexicographic order if the underlying LT α instance is
well-behaved. In particular, it should be irreflexive, asymmetric, and antisymmetric. These
requirements are precisely formulated in List.cons_le_cons_iff. If these hold, then as ≤ bs if
and only if:
-
as is empty, or
-
both as and bs are non-empty, and the head of as is less than the head of bs, or
-
both as and bs are non-empty, their heads are equal, and the tail of as is less than or
equal to the tail of bs.
🔗defList.lt.{u} {
α :
Type u} [
LT α] :
List α →
List α →
PropList.lt.{u} {
α :
Type u} [
LT α] :
List α →
List α →
Prop
Lexicographic ordering of lists with respect to an ordering on their elements.
as < bs if
-
as is empty and bs is non-empty, or
-
both as and bs are non-empty, and the head of as is less than the head of bs, or
-
both as and bs are non-empty, their heads are equal, and the tail of as is less than the
tail of bs.
🔗defList.lex.{u} {
α :
Type u} [
BEq α] (
l₁ l₂ :
List α)
(
lt :
α →
α →
Bool := by exact (· < ·)) :
BoolList.lex.{u} {
α :
Type u} [
BEq α]
(
l₁ l₂ :
List α)
(
lt :
α →
α →
Bool := by
exact (· < ·)) :
Bool
Compares lists lexicographically with respect to a comparison on their elements.
The lexicographic order with respect to lt is:
