-- This module is used to illustrate how to import a non-parameterised module.
module examples.syntax.ModuleA where

  data Nat : Set where
    zero  : Nat
    suc   : Nat -> Nat
    plus  : Nat -> Nat -> Nat

  eval : Nat -> Nat
  eval zero		    = zero
  eval (suc x)		    = suc (eval x)
  eval (plus zero y)	    = eval y
  eval (plus (suc x) y)	    = suc (eval (plus x y))
  eval (plus (plus x y) z)  = eval (plus x (plus y z))