module reductionSystems1 where


data Nat : Set where 
  Z : Nat  
  S : Nat -> Nat

infixl 60 _+_
infixl 80 _*_

_+_ : Nat -> Nat -> Nat
n + Z   = n
n + S m = S (n + m)

_*_ : Nat -> Nat -> Nat
n * Z   = Z
n * S m = n * m + n

{-# BUILTIN NATURAL  Nat  #-}
{-# BUILTIN ZERO     Z    #-}
{-# BUILTIN SUC      S    #-}
{-# BUILTIN NATPLUS  _+_  #-}
{-# BUILTIN NATTIMES _*_  #-}