module Nat where
open import Bool
{-
We begin by defining the data type of unary natural numbers
-}
data Nat : Set where
zero : Nat
succ : Nat → Nat
one = succ zero
two = succ one
{-
You can get access to decimal notation and machine arithmetic by using "builtin" numbers, see below.
Without machine arithmetic we define + and * by primitive recursion:
-}
_+_ : Nat → Nat → Nat
m + zero = m
m + succ n = succ (m + n)
_*_ : Nat → Nat → Nat
m * zero = zero
m * succ n = m + (m * n)
{-
We can declare precedences and associations in Agda. Here we can declare that both + and * are infix operations which associate to the left and that * binds harder than +:
-}
infixl 60 _+_
infixl 70 _*_
{-
Thus x + y + z parses as (x + y) + z:
-}
f : Nat → Nat → Nat → Nat
f x y z = x + y + z
{-
The following "pragma" declares that Nat corresponds to the computer's built-in natural numbers.
-}
{-# BUILTIN NATURAL Nat #-}
zerodecimal : Nat
zerodecimal = 0
{-
It also lets you write elements of Nat by using decimal notation. Moreover, if you write
-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-
you can use binary machine arithmetic for computing + and *.
There are many other built in types: integers, floats, strings, and characters. See the Agda wiki for more information.
Exercise:
(a) Define the factorial function
factorial : Nat → Nat
Compute the result of factorial for some instances by normalizing with ^C^N. How large factorials can Agda compute?
(b) Define the power function
power : Nat → Nat → Nat
--}
-- The equality test
_==_ : Nat → Nat → Bool
zero == zero = true
zero == succ n = false
succ m == zero = false
succ m == succ n = m == n