def Chapter13.fib₀ : Nat → Int

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 : Nat → Int) (lo hi : Nat) : Array Int

Equations

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

def Chapter13.fib₁ (n : Nat) : Int

Equations

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

@[irreducible]

def Chapter13.fib₁.a : Nat → Int

Equations

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

def Chapter13.fib₂ (n : Nat) : Int

Equations

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

def Chapter13.fib₂.apply (step : Int → Int → Int × Int) : Nat → Int × Int → Int × Int

Equations

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

def Chapter13.fact (n : Nat) : Int

Equations

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

def Chapter13.bin₀ (n r : Nat) : Int

Equations

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

def Chapter13.bin₁ : Nat → Nat → Int

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 : Nat) : Int

Equations

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

def Chapter13.apl {α : Type} : Nat → (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 : Nat) : Int

Equations

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