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