def Chapter3.SL1.nullSL {α : Type} : SymList α → Bool

Equations

• Chapter3.SL1.nullSL (xs, ys) = decide (xs.isEmpty = true ∧ ys.isEmpty = true)

def Chapter3.SL1.singleSL {α : Type} : SymList α → Prop

Equations

• Chapter3.SL1.singleSL (xs, ys) = (xs.isEmpty = true ∧ ys.single = true ∨ ys.isEmpty = true ∧ xs.single = true)

def Chapter3.SL1.lengthSL {α : Type} : SymList α → Nat

Equations

• Chapter3.SL1.lengthSL (xs, ys) = xs.length + ys.length

def Chapter3.SL1.headSL? {α : Type} : SymList α → Option α

Equations

• Chapter3.SL1.headSL? ([], []) = none
• Chapter3.SL1.headSL? ([], ys) = ys.head?
• Chapter3.SL1.headSL? (xs, snd) = xs.head?

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.length_lt_length_init {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

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

Equations

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

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

Equations

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

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

Equations

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

@[irreducible]

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

Equations

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

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

Equations

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

def Chapter3.updateT {α : Type} : Nat → α → Tree α → Tree α

Equations

• Chapter3.updateT 0 x✝ (Chapter3.Tree.leaf n) = Chapter3.Tree.leaf x✝
• Chapter3.updateT x✝¹ x✝ (Chapter3.Tree.leaf y) = Chapter3.Tree.leaf y
• Chapter3.updateT x✝¹ x✝ (Chapter3.Tree.node n t1 t2) = if x✝¹ < n / 2 then Chapter3.Tree.node n (Chapter3.updateT x✝¹ x✝ t1) t2 else Chapter3.Tree.node n t1 (Chapter3.updateT (x✝¹ - n / 2) x✝ t2)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Chapter3.fa₀ n = (Chapter1.scanl (fun (x1 x2 : Nat) => 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 (Nat × v) → Array e

Equations

• Chapter3.accum x✝¹ x✝ [] = x✝
• Chapter3.accum x✝¹ x✝ (p :: ps) = if h : p.fst < x✝.size then let i := ⟨p.fst, h⟩; Chapter3.accum x✝¹ (x✝.set (↑i) (x✝¹ x✝[i] p.snd) 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 : Nat) (is : List (Nat × v)) : Array a

Equations

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