def Chapter2.op1 {a : Type} : List a → a → a

Equations

• Chapter2.op1 [] x✝ = x✝
• Chapter2.op1 (x_2 :: tail) x✝ = x_2

def Chapter2.inits {a : Type u_1} (as : List a) : List (List a)

Equations

• Chapter2.inits as = Chapter2.inits.help id as

def Chapter2.inits.help {a : Type u_1} (f : List a → List a) : List a → List (List a)

Equations

• Chapter2.inits.help f [] = [f []]
• Chapter2.inits.help f (x_1 :: xs) = f [] :: Chapter2.inits.help (f ∘ List.cons x_1) xs

def Chapter2.tails1 {α : Type u_1} (xs : List α) : List (List α)

Equations

• Chapter2.tails1 xs = List.takeWhile (fun (x : List α) => decide ¬x.isEmpty = true) (Chapter2.iterate xs.length List.tail xs)