module exampleNat1 where


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


f : ℕ -> ℕ 
f n = f {! !}


g : ℕ -> ℕ 
g Z = Z
g (S n) = g n