Notation ℕ for the natural numbers.

def termℕ : Lean.ParserDescr

Equations

• termℕ = Lean.ParserDescr.node `termℕ 1024 (Lean.ParserDescr.symbol "ℕ")