module Nat where

data Nat : Type where
  Zero : Nat
  Succ : Nat -> Nat

plus : Nat -> Nat -> Nat
plus Zero m = m
plus (Succ n) m = Succ (plus n m)

mult : Nat -> Nat -> Nat
mult Zero m = Zero
mult (Succ n) m = plus m (mult n m)