module plus2 where

open import Data.Nat hiding (_+_)

_+_ : (x y : ℕ) → ℕ
x + zero = x
x + suc y = (suc x) + y

-- 10 + 20
-- 30