def Chapter2.fib : Nat → Nat

Equations

• Chapter2.fib 0 = 1
• Chapter2.fib 1 = 1
• Chapter2.fib n.succ.succ = Chapter2.fib (n + 1) + Chapter2.fib n

def Chapter2.fibFast (n : Nat) : Nat

Equations

• Chapter2.fibFast n = (Chapter2.fibFast.loop n).snd

def Chapter2.fibFast.loop : Nat → Nat × Nat

Equations

• Chapter2.fibFast.loop 0 = (0, 1)
• Chapter2.fibFast.loop n.succ = ((Chapter2.fibFast.loop n).snd, (Chapter2.fibFast.loop n).fst + (Chapter2.fibFast.loop n).snd)

def Chapter2.concat₀ {a : Type u_1} : List (List a) → List a

Equations

• Chapter2.concat₀ [] = []
• Chapter2.concat₀ (xs :: xss) = xs ++ Chapter2.concat₀ xss

def Chapter2.concat₁ {a : Type u_1} (xss : List (List a)) : List a

Equations

• Chapter2.concat₁ [] = []
• Chapter2.concat₁ (xs :: xss_1) = xs ++ Chapter2.concat₁ xss_1

def Chapter2.build {a : Type u_1} (p : a → a → Bool) : List a → List a

Equations

• Chapter2.build p = List.foldr (Chapter2.build.insert p) []

def Chapter2.build.insert {a : Type u_1} (p : a → a → Bool) (x : a) (xs : List a) : List a

Equations

• Chapter2.build.insert p x xs = x :: Chapter1.dropWhile (p x) xs

def Chapter2.iterate {a : Type u_1} : Nat → (a → a) → a → List a

Equations

• Chapter2.iterate 0 x✝¹ x✝ = [x✝]
• Chapter2.iterate n.succ x✝¹ x✝ = x✝ :: Chapter2.iterate n x✝¹ (x✝¹ x✝)

def Chapter2.bits (n : Nat) : List (List Bool)

Equations

• Chapter2.bits n = Chapter2.iterate n Chapter2.bits.inc []

def Chapter2.bits.inc : List Bool → List Bool

Equations

• Chapter2.bits.inc [] = [true]
• Chapter2.bits.inc (false :: bs) = true :: bs
• Chapter2.bits.inc (true :: bs) = false :: Chapter2.bits.inc bs

def Chapter2.init₀ {α : Type u_1} : List α → List α

Equations

• Chapter2.init₀ [] = panicWithPosWithDecl "Fad.Chapter2" "Chapter2.init₀" 105 13 "no elements"
• Chapter2.init₀ [head] = []
• Chapter2.init₀ (x_1 :: xs) = x_1 :: Chapter2.init₀ xs

def Chapter2.init₁ {α : Type u_1} : List α → Option (List α)

Equations

• Chapter2.init₁ [] = none
• Chapter2.init₁ [head] = some []
• Chapter2.init₁ (x_1 :: xs) = match Chapter2.init₁ xs with | none => none | some ys => some (x_1 :: ys)

def Chapter2.init₂ {α : Type u_1} : List α → Option (List α)

Equations

• Chapter2.init₂ [] = none
• Chapter2.init₂ [head] = some []
• Chapter2.init₂ (x_1 :: xs) = do let ys ← Chapter2.init₂ xs pure (x_1 :: ys)

def Chapter2.prune {a : Type u_1} (p : List a → Bool) (xs : List a) : List a

Equations

• Chapter2.prune p xs = List.foldr (Chapter2.prune.cut p) [] xs

def Chapter2.prune.cut {a : Type u_1} (p : List a → Bool) (x : a) (xs : List a) : List a

Equations

• Chapter2.prune.cut p x xs = Chapter1.until' (Chapter2.prune.done p) Chapter2.init₀ (x :: xs)

def Chapter2.prune.done {a : Type u_1} (p : List a → Bool) (xs : List a) : Bool

Equations

• Chapter2.prune.done p xs = decide (xs.isEmpty = true ∨ p xs = true)

def Chapter2.ordered : List Nat → Bool

Equations

• Chapter2.ordered [] = true
• Chapter2.ordered [head] = true
• Chapter2.ordered (x_1 :: y :: xs) = decide (x_1 ≤ y ∧ Chapter2.ordered (y :: xs) = true)