def Chapter3.abcd : List Char

Equations

• Chapter3.abcd = "abcd".toList

def Chapter3.SymList.initSL {a : Type} (sl : SymList a) : SymList a

Equations

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

theorem Chapter3.SymList.lengthSL_gt_lengthSL_initSL {a : Type} (sl : SymList a) (h : sl ≠ nil) : sl.lengthSL > sl.initSL.lengthSL

@[irreducible]

def Chapter3.SymList.initsSL {a : Type} (sl : SymList a) : SymList (SymList a)

Equations

• sl.initsSL = if h : sl.isEmpty = true then Chapter3.SymList.snocSL sl Chapter3.SymList.nil else have this := ⋯; Chapter3.SymList.snocSL sl sl.initSL.initsSL

theorem Chapter3.SymList.fromSL_splitInTwoSL {a : Type} (xs : List a) : (splitInTwoSL xs).fromSL = xs

theorem Chapter3.SymList.fromSL_initSL_eq_dropLast_fromSL {a : Type} : fromSL ∘ initSL = List.dropLast ∘ fromSL

theorem Chapter3.SymList.inits_eq_inits_dropLast_append {a : Type} (l : List a) (h : l ≠ []) : l.inits = l.dropLast.inits ++ [l]

theorem Chapter3.SymList.initsSL_eq_inits {a : Type} : List.inits ∘ fromSL = List.map fromSL ∘ fromSL ∘ initsSL

def Chapter3.inits {α : Type} : List α → List (List α)

Equations

• Chapter3.inits = List.map List.reverse ∘ Chapter1.scanl (flip List.cons) []

def Chapter3.RAList.measure {a : Type} (ts : List (Tree a)) : ℕ

Equations

• Chapter3.RAList.measure ts = List.foldr (fun (t : Chapter3.RAList.Tree a) (acc : ℕ) => Chapter3.RAList.measure.size t + acc) 0 ts

def Chapter3.RAList.measure.size {a : Type} : Tree a → ℕ

Equations

• Chapter3.RAList.measure.size (Chapter3.RAList.Tree.leaf n) = 1
• Chapter3.RAList.measure.size (Chapter3.RAList.Tree.node n t1 t2) = 1 + Chapter3.RAList.measure.size t1 + Chapter3.RAList.measure.size t2

@[irreducible]

def Chapter3.RAList.fromTs {a : Type} : List (Tree a) → List a

Equations

• Chapter3.RAList.fromTs [] = []
• Chapter3.RAList.fromTs (Chapter3.RAList.Tree.leaf x_1 :: ts) = x_1 :: Chapter3.RAList.fromTs ts
• Chapter3.RAList.fromTs (Chapter3.RAList.Tree.node n t1 t2 :: ts) = Chapter3.RAList.fromTs (t1 :: t2 :: ts)

def Chapter3.RAList.toRA {a : Type} : List a → RAList a

Equations

• Chapter3.RAList.toRA = List.foldr Chapter3.RAList.consRA Chapter3.RAList.nilRA

theorem Chapter3.RAList.fromRA_consT {a : Type} (t : Tree a) (ds : RAList a) : (consRA.consT t ds).fromRA = fromT t ++ ds.fromRA

theorem Chapter3.RAList.fromRA_consT' {a : Type} (t : Tree a) (ds : RAList a) : (consRA.consT t ds).fromRA = fromT t ++ ds.fromRA

def Chapter3.RAList.updateT {α : Type} : ℕ → α → Tree α → Tree α

Equations

• One or more equations did not get rendered due to their size.
• Chapter3.RAList.updateT 0 x✝ (Chapter3.RAList.Tree.leaf n) = Chapter3.RAList.Tree.leaf x✝
• Chapter3.RAList.updateT x✝¹ x✝ (Chapter3.RAList.Tree.leaf y) = Chapter3.RAList.Tree.leaf y

def Chapter3.RAList.updateRA {α : Type} : ℕ → α → RAList α → RAList α

Equations

• One or more equations did not get rendered due to their size.
• Chapter3.RAList.updateRA x✝¹ x✝ [] = []
• Chapter3.RAList.updateRA x✝¹ x✝ (Chapter3.RAList.Digit.zero :: xs) = Chapter3.RAList.Digit.zero :: Chapter3.RAList.updateRA x✝¹ x✝ xs

def Chapter3.RAList.updatesRA {α : Type} : RAList α → List (ℕ × α) → RAList α

Equations

• x✝¹.updatesRA x✝ = List.foldl (flip (Function.uncurry Chapter3.RAList.updateRA)) x✝¹ x✝

def Chapter3.RAList.unconsT {a : Type} : RAList a → Option (Tree a × RAList a)

Equations

• One or more equations did not get rendered due to their size.
• Chapter3.RAList.unconsT [] = none
• Chapter3.RAList.unconsT (Chapter3.RAList.Digit.one t :: xs) = if xs.isEmpty = true then some (t, []) else some (t, Chapter3.RAList.Digit.zero :: xs)

def Chapter3.RAList.unconsRA {a : Type} (xs : RAList a) : Option (a × RAList a)

Equations

• xs.unconsRA = match xs.unconsT with | some (Chapter3.RAList.Tree.leaf x, ys) => some (x, ys) | some (Chapter3.RAList.Tree.node n t₁ t₂, snd) => none | none => none

def Chapter3.RAList.headRA {a : Type} (xs : RAList a) : Option a

Equations

• xs.headRA = Prod.fst <$> xs.unconsRA

def Chapter3.RAList.tailRA {a : Type} (xs : RAList a) : Option (RAList a)

Equations

• xs.tailRA = Prod.snd <$> xs.unconsRA

def Chapter3.fa₀ (n : ℕ) : Array ℕ

Equations

• Chapter3.fa₀ n = (Chapter1.scanl (fun (x1 x2 : ℕ) => x1 * x2) 1 (List.range' 1 n)).toArray

def Chapter3.accum {e : Type u_1} {v : Type u_2} : (e → v → e) → Array e → List (ℕ × v) → Array e

Equations

• Chapter3.accum x✝¹ x✝ [] = x✝
• Chapter3.accum x✝¹ x✝ (p :: ps) = if h : p.1 < x✝.size then let i := ⟨p.1, h⟩; Chapter3.accum x✝¹ (x✝.set (↑i) (x✝¹ x✝[i] p.2) h) ps else Chapter3.accum x✝¹ x✝ ps

def Chapter3.accumArray₁ {a : Type u_1} {v : Type u_2} (f : a → v → a) (e : a) (n : ℕ) (is : List (ℕ × v)) : Array a

Equations

• Chapter3.accumArray₁ f e n is = Chapter3.accum f (Array.replicate n e) is