module exampleLetExpression where


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


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


infixl 40 _+_ 
infixl 50 _*_ 

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


f : N -> N
f n = let 
        m : N
        m = n + n
      in m * m