def Chapter0.hello₁ : String

Equations

• Chapter0.hello₁ = "Hello world!"

def Chapter0.hello₂ (s : String) : String

Equations

• Chapter0.hello₂ s = toString "Hello " ++ toString s ++ toString "!"

@[irreducible]

def Chapter0.factorial₀ (n : Nat) : Nat

Equations

• Chapter0.factorial₀ n = if n = 0 then 1 else n * Chapter0.factorial₀ (n - 1)

@[irreducible]

def Chapter0.factorial₁ (n : Nat) : Nat

Equations

• Chapter0.factorial₁ n = if n ≤ 0 then 1 else n * Chapter0.factorial₁ (n - 1)

@[irreducible]

def Chapter0.factorial₂ (n : Nat) : Nat

Equations

• Chapter0.factorial₂ n = if h : (n == 0) = true then 1 else have this := ⋯; n * Chapter0.factorial₂ (n - 1)

def Chapter0.factorial₃ : Nat → Nat

Equations

• Chapter0.factorial₃ 0 = 1
• Chapter0.factorial₃ n.succ = Chapter0.factorial₃ n * (n + 1)