The example with even and odd

Thomas Hallgren

November 2, 2000

1 The example with even and odd

First we define types for truth values and natural numbers. We then define the two mutually recursive functions even and odd. Bool ∈ Set Bool ≡ data \{ \begin{matrix}False \\ True \end{matrix} \}

Nat ∈ Set

Nat ≡ data \{ \begin{matrix}Zero \\ Succ & (n ∈ Nat) \end{matrix} \}

even ∈ (a ∈ Nat) → Bool

even ≡ λ a → case a of \{ \begin{matrix}Zero → True \\ Succ n → odd n \end{matrix} \}

odd ∈ (a ∈ Nat) → Bool odd ≡ λ a → case a of \{ \begin{matrix}Zero → False \\ Succ n → even n \end{matrix} \}