def Chapter13.fib₀ : ℕ → ℤ

Equations

• Chapter13.fib₀ 0 = 0
• Chapter13.fib₀ 1 = 1
• Chapter13.fib₀ n.succ.succ = Chapter13.fib₀ (n + 1) + Chapter13.fib₀ n

def Chapter13.tab (f : ℕ → ℤ) (lo hi : ℕ) : Array ℤ

Equations

• Chapter13.tab f lo hi = (List.map (fun (i : ℕ) => f (lo + i)) (List.range (hi - lo + 1))).toArray

def Chapter13.fib₁ (n : ℕ) : ℤ

Equations

• Chapter13.fib₁ n = (Chapter13.tab Chapter13.fib₁.a 0 n)[n]!

@[irreducible]

def Chapter13.fib₁.a : ℕ → ℤ

Equations

• Chapter13.fib₁.a a✝ = if a✝ ≤ 1 then ↑a✝ else Chapter13.fib₁.a (a✝ - 1) + Chapter13.fib₁.a (a✝ - 2)

def Chapter13.fib₂ (n : ℕ) : ℤ

Equations

• Chapter13.fib₂ n = match Chapter13.fib₂.apply (fun (a b : ℤ) => (b, a + b)) n (0, 1) with | (a, snd) => a

def Chapter13.fib₂.apply (step : ℤ → ℤ → ℤ × ℤ) : ℕ → ℤ × ℤ → ℤ × ℤ

Equations

• Chapter13.fib₂.apply step 0 a✝ = a✝
• Chapter13.fib₂.apply step n.succ (a, b) = Chapter13.fib₂.apply step n (step a b)

def Chapter13.fact (n : ℕ) : ℤ

Equations

• Chapter13.fact n = List.foldl (fun (x1 x2 : ℤ) => x1 * x2) 1 (List.map Int.ofNat (List.drop 1 (List.range (n + 1))))

def Chapter13.bin₀ (n r : ℕ) : ℤ

Equations

• Chapter13.bin₀ n r = Chapter13.fact n / (Chapter13.fact r * Chapter13.fact (n - r))

def Chapter13.bin₁ : ℕ → ℕ → ℤ

Equations

• Chapter13.bin₁ x✝ 0 = 1
• Chapter13.bin₁ 0 x✝ = 0
• Chapter13.bin₁ n.succ r.succ = if r + 1 = n + 1 then 1 else Chapter13.bin₁ n (r + 1) + Chapter13.bin₁ n r

def Chapter13.bin₂ (n r : ℕ) : ℤ

Equations

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

def Chapter13.apl {α : Type} : ℕ → (List α → List α) → List α → List α

Equations

• Chapter13.apl 0 x✝¹ x✝ = x✝
• Chapter13.apl n.succ x✝¹ x✝ = Chapter13.apl n x✝¹ (x✝¹ x✝)

def Chapter13.bin₃ (n r : ℕ) : ℤ

Equations

• Chapter13.bin₃ n r = (Chapter13.apl (n - r) (Chapter1.scanr₀ (fun (x1 x2 : ℤ) => x1 + x2) 0) (List.replicate (r + 1) 1)).headD 1