Programming Language Foundations in Agda: Naturals

Naturals.agda

module Naturals where

-- Funny, but the "Naturals" module only contains "Bin", because the other
-- exercises in this chapter were too trivial and boring to be worth doing.

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)

data Bin : Set where
  <> : Bin
  _O : Bin → Bin
  _I : Bin → Bin

infixl 10 _O
infixl 10 _I

inc : Bin → Bin
inc <>    = <> I
inc (x O) = x I
inc (x I) = (inc x) O

to : ℕ → Bin
to zero    = <> O
to (suc x) = inc (to x)

from : Bin → ℕ
from <>    = zero
from (x O) = 2 * from x
from (x I) = 1 + 2 * from x