def Auto.List.ofFun {α : Type u_1} (f : Nat → α) (n : Nat) : List α

This function is slow and is not meant to be used in computation It's main use is in the pushs_pops theorems

Equations

• Auto.List.ofFun f 0 = []
• Auto.List.ofFun f n'.succ = f 0 :: Auto.List.ofFun (fun (n : Nat) => f n.succ) n'

theorem Auto.List.ofFun_length {α : Type u_1} (f : Nat → α) (n : Nat) : (ofFun f n).length = n

theorem Auto.List.ofFun_getElem?_eq_some {α : Type u_1} (f : Nat → α) (n m : Nat) (h : n > m) : (ofFun f n)[m]? = some (f m)

theorem Auto.List.beq_def {α : Type u_1} [BEq α] {x y : List α} : (x == y) = x.beq y

theorem Auto.List.beq_refl {α : Type u_1} [BEq α] (H : ∀ (x : α), (x == x) = true) {l : List α} : (l == l) = true

theorem Auto.List.eq_of_beq_eq_true {α : Type u_1} [BEq α] (H : ∀ (x y : α), (x == y) = true → x = y) {l₁ l₂ : List α} : (l₁ == l₂) = true → l₁ = l₂

@[simp]

theorem Auto.List.getD_cons_zero {α : Type u_1} (x : α) (xs : List α) (d : α) : (x :: xs).getD 0 d = x

@[simp]

theorem Auto.List.getD_cons_succ {α : Type u_1} (x : α) (xs : List α) (d : α) {n : Nat} : (x :: xs).getD (n + 1) d = xs.getD n d

theorem Auto.List.getD_eq_get {α : Type u_1} (l : List α) (d : α) {n : Nat} (hn : n < l.length) : l.getD n d = l.get ⟨n, hn⟩

def Auto.List.split {α : Type u_1} : List α → List α × List α

Equations

• Auto.List.split [] = ([], [])
• Auto.List.split (a :: l) = match Auto.List.split l with | (l₁, l₂) => (a :: l₂, l₁)

theorem Auto.List.split_cons_of_eq {α : Type u_1} (a : α) {l l₁ l₂ : List α} (h : split l = (l₁, l₂)) : split (a :: l) = (a :: l₂, l₁)

theorem Auto.List.length_split_le {α : Type u_1} {l l₁ l₂ : List α} : split l = (l₁, l₂) → l₁.length ≤ l.length ∧ l₂.length ≤ l.length

theorem Auto.List.length_split_lt {α : Type u_1} {a b : α} {l l₁ l₂ : List α} (h : split (a :: b :: l) = (l₁, l₂)) : l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length

@[irreducible]

def Auto.List.merge {α : Type u_1} (r : α → α → Prop) [DecidableRel r] : List α → List α → List α

Equations

• Auto.List.merge r [] x✝ = x✝
• Auto.List.merge r x✝ [] = x✝
• Auto.List.merge r (a :: l) (b :: l') = if r a b then a :: Auto.List.merge r l (b :: l') else b :: Auto.List.merge r (a :: l) l'

@[irreducible]

def Auto.List.mergeSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] : List α → List α

Equations

• Auto.List.mergeSort r [] = []
• Auto.List.mergeSort r [a] = [a]
• Auto.List.mergeSort r (a :: b :: l) = Auto.List.merge r (Auto.List.mergeSort r (Auto.List.split (a :: b :: l)).fst) (Auto.List.mergeSort r (Auto.List.split (a :: b :: l)).snd)

theorem Auto.List.map_equiv {α : Type u_1} {β : Type u_2} {xs : List α} (f₁ f₂ : α → β) (hequiv : ∀ (x : α), f₁ x = f₂ x) : List.map f₁ xs = List.map f₂ xs

theorem Auto.List.length_reverseAux {α : Type u_1} (l₁ l₂ : List α) : (l₁.reverseAux l₂).length = l₁.length + l₂.length

def Auto.List.reverse_IsomType {α : Type u_1} : IsomType (List α) (List α)

Equations

• Auto.List.reverse_IsomType = { f := List.reverse, g := List.reverse, eq₁ := ⋯, eq₂ := ⋯ }