# Documentation

## Tail recursive implementations for List definitions. #

Many of the proofs require theorems about Array, so these are in a separate file to minimize imports.

@[inline]
def List.setTR {α : Type u_1} (l : List α) (n : Nat) (a : α) :
List α

Tail recursive version of erase.

Equations
Instances For
def List.setTR.go {α : Type u_1} (l : List α) (a : α) :
List αNatList α

Auxiliary for setTR: setTR.go l a xs n acc = acc.toList ++ set xs a, unless n ≥ l.length in which case it returns l

Equations
Instances For
@[csimp]
theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : ) (xs : List α) (n : Nat) :
l = acc.data ++ xsList.setTR.go l a xs n acc = acc.data ++ xs.set n a
@[inline]
def List.eraseTR {α : Type u_1} [BEq α] (l : List α) (a : α) :
List α

Tail recursive version of erase.

Equations
Instances For
def List.eraseTR.go {α : Type u_1} [BEq α] (l : List α) (a : α) :
List αList α

Auxiliary for eraseTR: eraseTR.go l a xs acc = acc.toList ++ erase xs a, unless a is not present in which case it returns l

Equations
Instances For
@[csimp]
@[inline]
def List.eraseIdxTR {α : Type u_1} (l : List α) (n : Nat) :
List α

Tail recursive version of eraseIdx.

Equations
Instances For
def List.eraseIdxTR.go {α : Type u_1} (l : List α) :
List αNatList α

Auxiliary for eraseIdxTR: eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a, unless a is not present in which case it returns l

Equations
Instances For
@[csimp]
@[inline]
def List.bindTR {α : Type u_1} {β : Type u_2} (as : List α) (f : αList β) :
List β

Tail recursive version of bind.

Equations
Instances For
@[specialize #[]]
def List.bindTR.go {α : Type u_1} {β : Type u_2} (f : αList β) :
List αList β

Auxiliary for bind: bind.go f as = acc.toList ++ bind f as

Equations
Instances For
@[csimp]
theorem List.bind_eq_bindTR.go (α : Type u_2) (β : Type u_1) (f : αList β) (as : List α) (acc : ) :
List.bindTR.go f as acc = acc.data ++ as.bind f
@[inline]
def List.joinTR {α : Type u_1} (l : List (List α)) :
List α

Tail recursive version of join.

Equations
• l.joinTR = l.bindTR id
Instances For
@[csimp]
@[inline]
def List.filterMapTR {α : Type u_1} {β : Type u_2} (f : α) (l : List α) :
List β

Tail recursive version of filterMap.

Equations
Instances For
@[specialize #[]]
def List.filterMapTR.go {α : Type u_1} {β : Type u_2} (f : α) :
List αList β

Auxiliary for filterMap: filterMap.go f l = acc.toList ++ filterMap f l

Equations
Instances For
@[csimp]
theorem List.filterMap_eq_filterMapTR.go (α : Type u_2) (β : Type u_1) (f : α) (as : List α) (acc : ) :
List.filterMapTR.go f as acc = acc.data ++
@[inline]
def List.replaceTR {α : Type u_1} [BEq α] (l : List α) (b : α) (c : α) :
List α

Tail recursive version of replace.

Equations
Instances For
@[specialize #[]]
def List.replaceTR.go {α : Type u_1} [BEq α] (l : List α) (b : α) (c : α) :
List αList α

Auxiliary for replace: replace.go l b c xs acc = acc.toList ++ replace xs b c, unless b is not found in xs in which case it returns l.

Equations
Instances For
@[csimp]
@[inline]
def List.takeTR {α : Type u_1} (n : Nat) (l : List α) :
List α

Tail recursive version of take.

Equations
Instances For
@[specialize #[]]
def List.takeTR.go {α : Type u_1} (l : List α) :
List αNatList α

Auxiliary for take: take.go l xs n acc = acc.toList ++ take n xs, unless n ≥ xs.length in which case it returns l.

Equations
Instances For
@[csimp]
@[inline]
def List.takeWhileTR {α : Type u_1} (p : αBool) (l : List α) :
List α

Tail recursive version of takeWhile.

Equations
Instances For
@[specialize #[]]
def List.takeWhileTR.go {α : Type u_1} (p : αBool) (l : List α) :
List αList α

Auxiliary for takeWhile: takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs, unless no element satisfying p is found in xs in which case it returns l.

Equations
Instances For
@[csimp]
@[specialize #[]]
def List.foldrTR {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (l : List α) :
β

Tail recursive version of foldr.

Equations
Instances For
@[csimp]
@[inline]
def List.zipWithTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : List α) (bs : List β) :
List γ

Tail recursive version of zipWith.

Equations
Instances For
def List.zipWithTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
List αList βList γ

Auxiliary for zipWith: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs

Equations
Instances For
@[csimp]
theorem List.zipWith_eq_zipWithTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : αβγ) (as : List α) (bs : List β) (acc : ) :
List.zipWithTR.go f as bs acc = acc.data ++ List.zipWith f as bs
def List.unzipTR {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
List α × List β

Tail recursive version of unzip.

Equations
• l.unzipTR = List.foldr (fun (x : α × β) (x_1 : List α × List β) => match x with | (a, b) => match x_1 with | (al, bl) => (a :: al, b :: bl)) ([], []) l
Instances For
@[csimp]
def List.enumFromTR {α : Type u_1} (n : Nat) (l : List α) :
List (Nat × α)

Tail recursive version of enumFrom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[csimp]
theorem List.enumFrom_eq_enumFromTR.go (α : Type u_1) (l : List α) (n : Nat) :
let f := fun (a : α) (x : Nat × List (Nat × α)) => match x with | (n, acc) => (n - 1, (n - 1, a) :: acc); List.foldr f (n + l.length, []) l = (n, )
theorem List.replicateTR_loop_eq :
∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), = ++ acc
@[inline]
def List.dropLastTR {α : Type u_1} (l : List α) :
List α

Tail recursive version of dropLast.

Equations
• l.dropLastTR = ().pop.toList
Instances For
@[csimp]
def List.intersperseTR {α : Type u_1} (sep : α) :
List αList α

Tail recursive version of intersperse.

Equations
Instances For
@[csimp]
def List.intercalateTR {α : Type u_1} (sep : List α) :
List (List α)List α

Tail recursive version of intercalate.

Equations
Instances For
def List.intercalateTR.go {α : Type u_1} (sep : ) :
List αList (List α)List α

Auxiliary for intercalateTR: intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)

Equations
Instances For
@[csimp]
theorem List.intercalate_eq_intercalateTR.go (α : Type u_1) (sep : List α) {acc : } {x : List α} (xs : List (List α)) :
List.intercalateTR.go (List.toArray sep) x xs acc = acc.data ++ (List.intersperse sep (x :: xs)).join