not able to identify the issue

Stream: new members

[Sham S]

def f (x : ℕ) :=
  x + 3

#check f

on defining the above function getting this

failed to synthesize instance
  HAdd ℕ Nat (?m.9 x)

what is the issue?

[Kyle Miller]

The fact that the error shows both ℕ and Nat hints that you aren't importing anything that provides ℕ notation.