Documentation
Std
.
Lean
.
Name
Search
Google site search
Std
.
Lean
.
Name
source
Imports
Init
Imported by
Lean
.
Name
.
hasNum
source
def
Lean
.
Name
.
hasNum
:
Lean.Name
→
Bool
Returns true if the name has any numeric components.
Equations
Lean.Name.hasNum
Lean.Name.anonymous
=
false
Lean.Name.hasNum
(
Lean.Name.str
p
str
)
=
Lean.Name.hasNum
p
Lean.Name.hasNum
(
Lean.Name.num
pre
i
)
=
true
Instances For