Documentation
Mathlib
.
Init
.
Data
.
Nat
.
Notation
Search
Google site search
Mathlib
.
Init
.
Data
.
Nat
.
Notation
source
Imports
Init
Imported by
termℕ
Notation
ℕ
for the natural numbers.
#
source
def
termℕ
:
Lean.ParserDescr
Equations
termℕ
=
Lean.ParserDescr.node
`termℕ
1024
(
Lean.ParserDescr.symbol
"ℕ"
)
Instances For