def «term[_]» : Lean.ParserDescr

The syntax [a, b, c] is shorthand for a :: b :: c :: [], or List.cons a (List.cons b (List.cons c List.nil)). It allows conveniently constructing list literals.

For lists of length at least 64, an alternative desugaring strategy is used which uses let bindings as intermediates as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions. Note that this changes the order of evaluation, although it should not be observable unless you use side effecting operations like dbg_trace.

Equations

• One or more equations did not get rendered due to their size.

def «term%[_|_]» : Lean.ParserDescr

Auxiliary syntax for implementing [$elem,*] list literal syntax. The syntax %[a,b,c|tail] constructs a value equivalent to a::b::c::tail. It uses binary partitioning to construct a tree of intermediate let bindings as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions.

Equations

• One or more equations did not get rendered due to their size.

instance List.instGetElemListNatLtInstLTNatLength {α : Type u} : GetElem (List α) Nat α fun (as : List α) (i : Nat) => i < List.length as

Equations

• List.instGetElemListNatLtInstLTNatLength = { getElem := fun (as : List α) (i : Nat) (h : i < List.length as) => List.get as { val := i, isLt := h } }

@[simp]

theorem List.cons_getElem_zero {α : Type u} (a : α) (as : List α) (h : 0 < List.length (a :: as)) : (a :: as)[0] = a

@[simp]

theorem List.cons_getElem_succ {α : Type u} (a : α) (as : List α) (i : Nat) (h : i + 1 < List.length (a :: as)) : (a :: as)[i + 1] = as[i]

theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) : List.length as + n = List.lengthTRAux as n

@[csimp]

theorem List.length_eq_lengthTR : @List.length = @List.lengthTR

@[simp]

theorem List.length_nil {α : Type u} : List.length [] = 0

def List.reverseAux {α : Type u} : List α → List α → List α

Auxiliary for List.reverse. List.reverseAux l r = l.reverse ++ r, but it is defined directly.

Equations

• List.reverseAux [] x = x
• List.reverseAux (a :: l) x = List.reverseAux l (a :: x)

def List.reverse {α : Type u} (as : List α) : List α

O(|as|). Reverse of a list:

• [1, 2, 3, 4].reverse = [4, 3, 2, 1]

Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.

Equations

• List.reverse as = List.reverseAux as []

theorem List.reverseAux_reverseAux_nil {α : Type u} (as : List α) (bs : List α) : List.reverseAux (List.reverseAux as bs) [] = List.reverseAux bs as

theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) : List.reverseAux (List.reverseAux as bs) cs = List.reverseAux bs (List.reverseAux (List.reverseAux as []) cs)

@[simp]

theorem List.reverse_reverse {α : Type u} (as : List α) : List.reverse (List.reverse as) = as

def List.append {α : Type u} (xs : List α) (ys : List α) : List α

O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first list.

Equations

• List.append [] x = x
• List.append (a :: l) x = a :: List.append l x

def List.appendTR {α : Type u} (as : List α) (bs : List α) : List α

Tail-recursive version of List.append.

Equations

• List.appendTR as bs = List.reverseAux (List.reverse as) bs

@[csimp]

theorem List.append_eq_appendTR : @List.append = @List.appendTR

instance List.instAppendList {α : Type u} : Append (List α)

Equations

• List.instAppendList = { append := List.append }

@[simp]

theorem List.nil_append {α : Type u} (as : List α) : [] ++ as = as

@[simp]

theorem List.append_nil {α : Type u} (as : List α) : as ++ [] = as

@[simp]

theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) : a :: as ++ bs = a :: (as ++ bs)

@[simp]

theorem List.append_eq {α : Type u} (as : List α) (bs : List α) : List.append as bs = as ++ bs

@[simp]

theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) : as ++ bs ++ cs = as ++ (bs ++ cs)

theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs

instance List.instEmptyCollectionList {α : Type u} : EmptyCollection (List α)

Equations

• List.instEmptyCollectionList = { emptyCollection := [] }

def List.erase {α : Type u_1} [BEq α] : List α → α → List α

O(|l|). erase l a removes the first occurrence of a from l.

• erase [1, 5, 3, 2, 5] 5 = [1, 3, 2, 5]
• erase [1, 5, 3, 2, 5] 6 = [1, 5, 3, 2, 5]

Equations

• List.erase [] x = []
• List.erase (a :: as) x = match a == x with | true => as | false => a :: List.erase as x

def List.eraseIdx {α : Type u} : List α → Nat → List α

O(i). eraseIdx l i removes the i'th element of the list l.

• erase [a, b, c, d, e] 0 = [b, c, d, e]
• erase [a, b, c, d, e] 1 = [a, c, d, e]
• erase [a, b, c, d, e] 5 = [a, b, c, d, e]

Equations

• List.eraseIdx [] x = []
• List.eraseIdx (head :: as) 0 = as
• List.eraseIdx (a :: as) (Nat.succ n) = a :: List.eraseIdx as n

def List.isEmpty {α : Type u} : List α → Bool

O(1). isEmpty l is true if the list is empty.

• isEmpty [] = true
• isEmpty [a] = false
• isEmpty [a, b] = false

Equations

• List.isEmpty x = match x with | [] => true | head :: tail => false

@[specialize #[]]

def List.map {α : Type u} {β : Type v} (f : α → β) : List α → List β

O(|l|). map f l applies f to each element of the list.

• map f [a, b, c] = [f a, f b, f c]

Equations

• List.map f [] = []
• List.map f (head :: tail) = f head :: List.map f tail

@[inline]

def List.mapTR {α : Type u} {β : Type v} (f : α → β) (as : List α) : List β

Tail-recursive version of List.map.

Equations

• List.mapTR f as = List.mapTR.loop f as []

@[specialize #[]]

def List.mapTR.loop {α : Type u} {β : Type v} (f : α → β) : List α → List β → List β

Equations

• List.mapTR.loop f [] x = List.reverse x
• List.mapTR.loop f (a :: as) x = List.mapTR.loop f as (f a :: x)

theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) : List.reverseAux as bs = List.reverseAux as [] ++ bs

@[simp]

theorem List.reverse_nil {α : Type u} : List.reverse [] = []

@[simp]

theorem List.reverse_cons {α : Type u} (a : α) (as : List α) : List.reverse (a :: as) = List.reverse as ++ [a]

@[simp]

theorem List.reverse_append {α : Type u} (as : List α) (bs : List α) : List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as

theorem List.mapTR_loop_eq {α : Type u} {β : Type v} (f : α → β) (as : List α) (bs : List β) : List.mapTR.loop f as bs = List.reverse bs ++ List.map f as

@[csimp]

theorem List.map_eq_mapTR : @List.map = @List.mapTR

def List.join {α : Type u} : List (List α) → List α

O(|join L|). join L concatenates all the lists in L into one list.

• join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]

Equations

• List.join [] = []
• List.join (a :: as) = a ++ List.join as

@[specialize #[]]

def List.filterMap {α : Type u} {β : Type v} (f : α → Option β) : List α → List β

O(|l|). filterMap f l takes a function f : α → Option β and applies it to each element of l; the resulting non-none values are collected to form the output list.

filterMap
  (fun x => if x > 2 then some (2 * x) else none)
  [1, 2, 5, 2, 7, 7]
= [10, 14, 14]

Equations

• List.filterMap f [] = []
• List.filterMap f (head :: tail) = match f head with | none => List.filterMap f tail | some b => b :: List.filterMap f tail

def List.filter {α : Type u} (p : α → Bool) : List α → List α

O(|l|). filter f l returns the list of elements in l for which f returns true.

filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]

Equations

• List.filter p [] = []
• List.filter p (head :: tail) = match p head with | true => head :: List.filter p tail | false => List.filter p tail

@[inline]

def List.filterTR {α : Type u} (p : α → Bool) (as : List α) : List α

Tail-recursive version of List.filter.

Equations

• List.filterTR p as = List.filterTR.loop p as []

@[specialize #[]]

def List.filterTR.loop {α : Type u} (p : α → Bool) : List α → List α → List α

Equations

• List.filterTR.loop p [] x = List.reverse x
• List.filterTR.loop p (a :: l) x = match p a with | true => List.filterTR.loop p l (a :: x) | false => List.filterTR.loop p l x

theorem List.filterTR_loop_eq {α : Type u} (p : α → Bool) (as : List α) (bs : List α) : List.filterTR.loop p as bs = List.reverse bs ++ List.filter p as

@[csimp]

theorem List.filter_eq_filterTR : @List.filter = @List.filterTR

@[inline]

def List.partition {α : Type u} (p : α → Bool) (as : List α) : List α × List α

O(|l|). partition p l calls p on each element of l, partitioning the list into two lists (l_true, l_false) where l_true has the elements where p was true and l_false has the elements where p is false. partition p l = (filter p l, filter (not ∘ p) l), but it is slightly more efficient since it only has to do one pass over the list.

partition (· > 2) [1, 2, 5, 2, 7, 7] = ([5, 7, 7], [1, 2, 2])

Equations

• List.partition p as = List.partition.loop p as ([], [])

@[specialize #[]]

def List.partition.loop {α : Type u} (p : α → Bool) : List α → List α × List α → List α × List α

Equations

• List.partition.loop p [] (bs, cs) = (List.reverse bs, List.reverse cs)
• List.partition.loop p (a :: as) (bs, cs) = match p a with | true => List.partition.loop p as (a :: bs, cs) | false => List.partition.loop p as (bs, a :: cs)

def List.dropWhile {α : Type u} (p : α → Bool) : List α → List α

O(|l|). dropWhile p l removes elements from the list until it finds the first element for which p returns false; this element and everything after it is returned.

dropWhile (· < 4) [1, 3, 2, 4, 2, 7, 4] = [4, 2, 7, 4]

Equations

• List.dropWhile p [] = []
• List.dropWhile p (head :: tail) = match p head with | true => List.dropWhile p tail | false => head :: tail

def List.find? {α : Type u} (p : α → Bool) : List α → Option α

O(|l|). find? p l returns the first element for which p returns true, or none if no such element is found.

• find? (· < 5) [7, 6, 5, 8, 1, 2, 6] = some 1
• find? (· < 1) [7, 6, 5, 8, 1, 2, 6] = none

Equations

• List.find? p [] = none
• List.find? p (head :: tail) = match p head with | true => some head | false => List.find? p tail

def List.findSome? {α : Type u} {β : Type v} (f : α → Option β) : List α → Option β

O(|l|). findSome? f l applies f to each element of l, and returns the first non-none result.

• findSome? (fun x => if x < 5 then some (10 * x) else none) [7, 6, 5, 8, 1, 2, 6] = some 10

Equations

• List.findSome? f [] = none
• List.findSome? f (head :: tail) = match f head with | some b => some b | none => List.findSome? f tail

def List.replace {α : Type u} [BEq α] : List α → α → α → List α

O(|l|). replace l a b replaces the first element in the list equal to a with b.

• replace [1, 4, 2, 3, 3, 7] 3 6 = [1, 4, 2, 6, 3, 7]
• replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]

Equations

• List.replace [] x✝ x = []
• List.replace (a :: as) x✝ x = match a == x✝ with | true => x :: as | false => a :: List.replace as x✝ x

def List.elem {α : Type u} [BEq α] (a : α) : List α → Bool

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false

Equations

• List.elem a [] = false
• List.elem a (head :: tail) = match a == head with | true => true | false => List.elem a tail

def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) : Bool

notElem a l is !(elem a l).

Equations

• List.notElem a as = !List.elem a as

@[inline, reducible]

abbrev List.contains {α : Type u} [BEq α] (as : List α) (a : α) : Bool

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false

Equations

• List.contains as a = List.elem a as

inductive List.Mem {α : Type u} (a : α) : List α → Prop

a ∈ l is a predicate which asserts that a is in the list l. Unlike elem, this uses = instead of == and is suited for mathematical reasoning.

• a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z

• head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)

  The head of a list is a member: a ∈ a :: as.

• tail: ∀ {α : 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.

instance List.instMembershipList {α : Type u} : Membership α (List α)

Equations

• List.instMembershipList = { mem := List.Mem }

theorem List.mem_of_elem_eq_true {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} : List.elem a as = true → a ∈ as

theorem List.elem_eq_true_of_mem {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} (h : a ∈ as) : List.elem a as = true

instance List.instDecidableMemListInstMembershipList {α : Type u} [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a ∈ as)

Equations

• List.instDecidableMemListInstMembershipList a as = decidable_of_decidable_of_iff ⋯

theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs

theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs

def List.eraseDups {α : Type u_1} [BEq α] (as : List α) : List α

O(|l|^2). Erase duplicated elements in the list. Keeps the first occurrence of duplicated elements.

• eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]

Equations

• List.eraseDups as = List.eraseDups.loop as []

def List.eraseDups.loop {α : Type u_1} [BEq α] : List α → List α → List α

Equations

• List.eraseDups.loop [] x = List.reverse x
• List.eraseDups.loop (a :: l) x = match List.elem a x with | true => List.eraseDups.loop l x | false => List.eraseDups.loop l (a :: x)

def List.eraseReps {α : Type u_1} [BEq α] : List α → List α

O(|l|). Erase repeated adjacent elements. Keeps the first occurrence of each run.

• eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]

Equations

• List.eraseReps x = match x with | [] => [] | a :: as => List.eraseReps.loop a as []

def List.eraseReps.loop {α : Type u_1} [BEq α] : α → List α → List α → List α

Equations

• List.eraseReps.loop x✝ [] x = List.reverse (x✝ :: x)
• List.eraseReps.loop x✝ (a' :: as) x = match x✝ == a' with | true => List.eraseReps.loop x✝ as x | false => List.eraseReps.loop a' as (x✝ :: x)

@[inline]

def List.span {α : Type u} (p : α → Bool) (as : List α) : List α × List α

O(|l|). span p l splits the list l into two parts, where the first part contains the longest initial segment for which p returns true and the second part is everything else.

• 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], [])

Equations

• List.span p as = List.span.loop p as []

@[specialize #[]]

def List.span.loop {α : Type u} (p : α → Bool) : List α → List α → List α × List α

Equations

• List.span.loop p [] x = (List.reverse x, [])
• List.span.loop p (a :: l) x = match p a with | true => List.span.loop p l (a :: x) | false => (List.reverse x, a :: l)

@[specialize #[]]

def List.groupBy {α : Type u} (R : α → α → Bool) : List α → List (List α)

O(|l|). groupBy R l splits l into chains of elements such that adjacent elements are related by R.

• groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]
• groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]

Equations

• List.groupBy R x = match x with | [] => [] | a :: as => List.groupBy.loop R as a [] []

@[specialize #[]]

def List.groupBy.loop {α : Type u} (R : α → α → Bool) : List α → α → List α → List (List α) → List (List α)

Equations

• List.groupBy.loop R (a :: as) x✝¹ x✝ x = match R x✝¹ a with | true => List.groupBy.loop R as a (x✝¹ :: x✝) x | false => List.groupBy.loop R as a [] (List.reverse (x✝¹ :: x✝) :: x)
• List.groupBy.loop R [] x✝¹ x✝ x = List.reverse (List.reverse (x✝¹ :: x✝) :: x)

def List.lookup {α : Type u} {β : Type v} [BEq α] : α → List (α × β) → Option β

O(|l|). lookup a l treats l : List (α × β) like an association list, and returns the first β value corresponding to an α value in the list equal to a.

• lookup 3 [(1, 2), (3, 4), (3, 5)] = some 4
• lookup 2 [(1, 2), (3, 4), (3, 5)] = none

Equations

• List.lookup x [] = none
• List.lookup x ((k, b) :: es) = match x == k with | true => some b | false => List.lookup x es

def List.removeAll {α : Type u} [BEq α] (xs : List α) (ys : List α) : List α

O(|xs|). Computes the "set difference" of lists, by filtering out all elements of xs which are also in ys.

• removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]

Equations

• List.removeAll xs ys = List.filter (fun (x : α) => List.notElem x ys) xs

def List.drop {α : Type u} : Nat → List α → List α

O(min n |xs|). Removes the first n elements of xs.

• drop 0 [a, b, c, d, e] = [a, b, c, d, e]
• drop 3 [a, b, c, d, e] = [d, e]
• drop 6 [a, b, c, d, e] = []

Equations

• List.drop 0 x = x
• List.drop (Nat.succ n) [] = []
• List.drop (Nat.succ n) (head :: as) = List.drop n as

@[simp]

theorem List.drop_nil {α : Type u} {i : Nat} : List.drop i [] = []

theorem List.get_drop_eq_drop {α : Type u} (as : List α) (i : Nat) (h : i < List.length as) : as[i] :: List.drop (i + 1) as = List.drop i as

def List.take {α : Type u} : Nat → List α → List α

O(min n |xs|). Returns the first n elements of xs, or the whole list if n is too large.

• take 0 [a, b, c, d, e] = []
• take 3 [a, b, c, d, e] = [a, b, c]
• take 6 [a, b, c, d, e] = [a, b, c, d, e]

Equations

• List.take 0 x = []
• List.take (Nat.succ n) [] = []
• List.take (Nat.succ n) (head :: as) = head :: List.take n as

def List.takeWhile {α : Type u} (p : α → Bool) (xs : List α) : List α

O(|xs|). Returns the longest initial segment of xs for which p returns true.

• takeWhile (· > 5) [7, 6, 4, 8] = [7, 6]
• takeWhile (· > 5) [7, 6, 6, 8] = [7, 6, 6, 8]

Equations

• List.takeWhile p [] = []
• List.takeWhile p (head :: tail) = match p head with | true => head :: List.takeWhile p tail | false => []

@[specialize #[]]

def List.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) : List α → β

O(|l|). Applies function f to all of the elements of the list, from right to left.

• foldr f init [a, b, c] = f a <| f b <| f c <| init

Equations

• List.foldr f init [] = init
• List.foldr f init (head :: tail) = f head (List.foldr f init tail)

def List.any {α : Type u} : List α → (α → Bool) → Bool

O(|l|). Returns true if p is true for any element of l.

• any p [a, b, c] = p a || p b || p c

Short-circuits upon encountering the first true.

Equations

• List.any [] x = false
• List.any (h :: t) x = (x h || List.any t x)

def List.all {α : Type u} : List α → (α → Bool) → Bool

O(|l|). Returns true if p is true for every element of l.

• all p [a, b, c] = p a && p b && p c

Short-circuits upon encountering the first false.

Equations

• List.all [] x = true
• List.all (h :: t) x = (x h && List.all t x)

def List.or (bs : List Bool) : Bool

O(|l|). Returns true if true is an element of the list of booleans l.

• or [a, b, c] = a || b || c

Equations

• List.or bs = List.any bs id

def List.and (bs : List Bool) : Bool

O(|l|). Returns true if every element of l is the value true.

• and [a, b, c] = a && b && c

Equations

• List.and bs = List.all bs id

@[specialize #[]]

def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α) (ys : List β) : List γ

O(min |xs| |ys|). Applies f to the two lists in parallel, stopping at the shorter list.

• zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

Equations

• List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
• List.zipWith f x✝ x = []

def List.zip {α : Type u} {β : Type v} : List α → List β → List (α × β)

O(min |xs| |ys|). Combines the two lists into a list of pairs, with one element from each list. The longer list is truncated to match the shorter list.

• zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]

Equations

• List.zip = List.zipWith Prod.mk

def List.zipWithAll {α : Type u} {β : Type v} {γ : Type w} (f : Option α → Option β → γ) : List α → List β → List γ

O(max |xs| |ys|). Version of List.zipWith that continues to the end of both lists, passing none to one argument once the shorter list has run out.

Equations

• List.zipWithAll f [] x = List.map (fun (b : β) => f none (some b)) x
• List.zipWithAll f (a :: as) [] = List.map (fun (a : α) => f (some a) none) (a :: as)
• List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

@[simp]

theorem List.zipWithAll_nil_right : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as

@[simp]

theorem List.zipWithAll_nil_left : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs

@[simp]

theorem List.zipWithAll_cons_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

def List.unzip {α : Type u} {β : Type v} : List (α × β) → List α × List β

O(|l|). Separates a list of pairs into two lists containing the first components and second components.

• unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])

Equations

• List.unzip [] = ([], [])
• List.unzip ((a, b) :: t) = match List.unzip t with | (al, bl) => (a :: al, b :: bl)

def List.range (n : Nat) : List Nat

O(n). range n is the numbers from 0 to n exclusive, in increasing order.

• range 5 = [0, 1, 2, 3, 4]

Equations

• List.range n = List.range.loop n []

def List.range.loop : Nat → List Nat → List Nat

Equations

• List.range.loop 0 x = x
• List.range.loop (Nat.succ n) x = List.range.loop n (n :: x)

def List.iota : Nat → List Nat

O(n). iota n is the numbers from 1 to n inclusive, in decreasing order.

• iota 5 = [5, 4, 3, 2, 1]

Equations

• List.iota 0 = []
• List.iota (Nat.succ n) = Nat.succ n :: List.iota n

def List.iotaTR (n : Nat) : List Nat

Tail-recursive version of iota.

Equations

• List.iotaTR n = List.iotaTR.go n []

def List.iotaTR.go : Nat → List Nat → List Nat

Equations

• List.iotaTR.go 0 x = List.reverse x
• List.iotaTR.go (Nat.succ n) x = List.iotaTR.go n (Nat.succ n :: x)

@[csimp]

theorem List.iota_eq_iotaTR : List.iota = List.iotaTR

def List.enumFrom {α : Type u} : Nat → List α → List (Nat × α)

O(|l|). enumFrom n l is like enum but it allows you to specify the initial index.

• enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]

Equations

• List.enumFrom x [] = []
• List.enumFrom x (x_2 :: xs) = (x, x_2) :: List.enumFrom (x + 1) xs

def List.enum {α : Type u} : List α → List (Nat × α)

O(|l|). enum l pairs up each element with its index in the list.

• enum [a, b, c] = [(0, a), (1, b), (2, c)]

Equations

• List.enum = List.enumFrom 0

def List.intersperse {α : Type u} (sep : α) : List α → List α

O(|l|). intersperse sep l alternates sep and the elements of l:

• intersperse sep [] = []
• intersperse sep [a] = [a]
• intersperse sep [a, b] = [a, sep, b]
• intersperse sep [a, b, c] = [a, sep, b, sep, c]

Equations

• List.intersperse sep [] = []
• List.intersperse sep [x_1] = [x_1]
• List.intersperse sep (x_1 :: xs) = x_1 :: sep :: List.intersperse sep xs

def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) : List α

O(|xs|). intercalate sep xs alternates sep and the elements of xs:

• intercalate sep [] = []
• intercalate sep [a] = a
• intercalate sep [a, b] = a ++ sep ++ b
• intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c

Equations

• List.intercalate sep xs = List.join (List.intersperse sep xs)

@[inline]

def List.bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β

bind xs f is the bind operation of the list monad. It applies f to each element of xs to get a list of lists, and then concatenates them all together.

• [2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]

Equations

• List.bind a b = List.join (List.map b a)

@[inline]

def List.pure {α : Type u} (a : α) : List α

pure x = [x] is the pure operation of the list monad.

Equations

• List.pure a = [a]

inductive List.lt {α : Type u} [LT α] : List α → List α → Prop

The lexicographic order on lists. [] < a::as, and a::as < b::bs if a < b or if a and b are equivalent and as < bs.

• nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)

  [] is the smallest element in the order.

• head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → List.lt (a :: as) (b :: bs)

  If a < b then a::as < b::bs.

• tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b → ¬b < a → List.lt as bs → List.lt (a :: as) (b :: bs)

  If a and b are equivalent and as < bs, then a::as < b::bs.

instance List.instLTList {α : Type u} [LT α] : LT (List α)

Equations

• List.instLTList = { lt := List.lt }

instance List.hasDecidableLt {α : Type u} [LT α] [h : DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) : Decidable (l₁ < l₂)

Equations

• One or more equations did not get rendered due to their size.
• List.hasDecidableLt [] [] = isFalse ⋯
• List.hasDecidableLt [] (head :: tail) = isTrue ⋯
• List.hasDecidableLt (head :: tail) [] = isFalse ⋯

@[reducible]

def List.le {α : Type u} [LT α] (a : List α) (b : List α) : Prop

The lexicographic order on lists.

Equations

• List.le a b = ¬b < a

instance List.instLEList {α : Type u} [LT α] : LE (List α)

Equations

• List.instLEList = { le := List.le }

instance List.instForAllListDecidableLeInstLEList {α : Type u} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) : Decidable (l₁ ≤ l₂)

Equations

• List.instForAllListDecidableLeInstLEList x✝ x = inferInstanceAs (Decidable ¬x < x✝)

def List.isPrefixOf {α : Type u} [BEq α] : List α → List α → Bool

isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

Equations

• List.isPrefixOf [] x = true
• List.isPrefixOf x [] = false
• List.isPrefixOf (a :: as) (b :: bs) = (a == b && List.isPrefixOf as bs)

def List.isPrefixOf? {α : Type u} [BEq α] : List α → List α → Option (List α)

isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

Equations

• List.isPrefixOf? [] x = some x
• List.isPrefixOf? x [] = none
• List.isPrefixOf? (a :: as) (b :: bs) = if (a == b) = true then List.isPrefixOf? as bs else none

def List.isSuffixOf {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) : Bool

isSuffixOf l₁ l₂ returns true Iff l₁ is a suffix of l₂. That is, there exists a t such that l₂ == t ++ l₁.

Equations

• List.isSuffixOf l₁ l₂ = List.isPrefixOf (List.reverse l₁) (List.reverse l₂)

def List.isSuffixOf? {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) : Option (List α)

isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

Equations

• List.isSuffixOf? l₁ l₂ = Option.map List.reverse (List.isPrefixOf? (List.reverse l₁) (List.reverse l₂))

@[specialize #[]]

def List.isEqv {α : Type u} (as : List α) (bs : List α) (eqv : α → α → Bool) : Bool

O(min |as| |bs|). Returns true if as and bs have the same length, and they are pairwise related by eqv.

Equations

• List.isEqv [] [] x = true
• List.isEqv (a :: as) (b :: bs) x = (x a b && List.isEqv as bs x)
• List.isEqv x✝¹ x✝ x = false

def List.beq {α : Type u} [BEq α] : List α → List α → Bool

The equality relation on lists asserts that they have the same length and they are pairwise BEq.

Equations

• List.beq [] [] = true
• List.beq (a :: as) (b :: bs) = (a == b && List.beq as bs)
• List.beq x✝ x = false

instance List.instBEqList {α : Type u} [BEq α] : BEq (List α)

Equations

• List.instBEqList = { beq := List.beq }

def List.replicate {α : Type u} (n : Nat) (a : α) : List α

replicate n a is n copies of a:

• replicate 5 a = [a, a, a, a, a]

Equations

• List.replicate 0 x = []
• List.replicate (Nat.succ n) x = x :: List.replicate n x

def List.replicateTR {α : Type u} (n : Nat) (a : α) : List α

Tail-recursive version of List.replicate.

Equations

• List.replicateTR n a = List.replicateTR.loop a n []

def List.replicateTR.loop {α : Type u} (a : α) : Nat → List α → List α

Equations

• List.replicateTR.loop a 0 x = x
• List.replicateTR.loop a (Nat.succ n) x = List.replicateTR.loop a n (a :: x)

theorem List.replicateTR_loop_replicate_eq {α : Type u} (a : α) (m : Nat) (n : Nat) : List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a

@[csimp]

theorem List.replicate_eq_replicateTR : @List.replicate = @List.replicateTR

def List.dropLast {α : Type u_1} : List α → List α

Removes the last element of the list.

• dropLast [] = []
• dropLast [a] = []
• dropLast [a, b, c] = [a, b]

Equations

• List.dropLast [] = []
• List.dropLast [x_1] = []
• List.dropLast (x_1 :: xs) = x_1 :: List.dropLast xs

@[simp]

theorem List.length_replicate {α : Type u} (n : Nat) (a : α) : List.length (List.replicate n a) = n

@[simp]

theorem List.length_concat {α : Type u} (as : List α) (a : α) : List.length (List.concat as a) = List.length as + 1

@[simp]

theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) : List.length (List.set as i a) = List.length as

@[simp]

theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) : List.length (List.dropLast (a :: as)) = List.length as

@[simp]

theorem List.length_append {α : Type u} (as : List α) (bs : List α) : List.length (as ++ bs) = List.length as + List.length bs

@[simp]

theorem List.length_map {α : Type u} {β : Type v} (as : List α) (f : α → β) : List.length (List.map f as) = List.length as

@[simp]

theorem List.length_reverse {α : Type u} (as : List α) : List.length (List.reverse as) = List.length as

def List.maximum? {α : Type u} [Max α] : List α → Option α

Returns the largest element of the list, if it is not empty.

• [].maximum? = none
• [4].maximum? = some 4
• [1, 4, 2, 10, 6].maximum? = some 10

Equations

• List.maximum? x = match x with | [] => none | a :: as => some (List.foldl max a as)

def List.minimum? {α : Type u} [Min α] : List α → Option α

Returns the smallest element of the list, if it is not empty.

• [].minimum? = none
• [4].minimum? = some 4
• [1, 4, 2, 10, 6].minimum? = some 1

Equations

• List.minimum? x = match x with | [] => none | a :: as => some (List.foldl min a as)

@[inline]

def List.insert {α : Type u} [BEq α] (a : α) (l : List α) : List α

Inserts an element into a list without duplication.

Equations

• List.insert a l = if List.elem a l = true then l else a :: l

instance List.decidableBEx {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) : Decidable (∃ (x : α), x ∈ l ∧ p x)

Equations

• List.decidableBEx p [] = isFalse ⋯
• List.decidableBEx p (head :: tail) = if h₁ : p head then isTrue ⋯ else match List.decidableBEx p tail with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯

instance List.decidableBAll {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) : Decidable (∀ (x : α), x ∈ l → p x)

Equations

• List.decidableBAll p [] = isTrue ⋯
• List.decidableBAll p (head :: tail) = if h₁ : p head then match List.decidableBAll p tail with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯ else isFalse ⋯

instance List.instLawfulBEqListInstBEqList {α : Type u} [BEq α] [LawfulBEq α] : LawfulBEq (List α)

Equations

• ⋯ = ⋯

theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : List.concat as a = List.concat bs b) : as = bs ∧ a = b

@[simp]

theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) : List.concat as a = as ++ [a]

theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : List.length as ≤ i) : List.drop i as = []