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

def Lean.Name.isInternalOrNum : Lean.Name → Bool

The frontend does not allow user declarations to start with _ in any of its parts. We use name parts starting with _ internally to create auxiliary names (e.g., _private).

Equations

• Lean.Name.isInternalOrNum (Lean.Name.str p s) = (String.get s 0 == Char.ofNat 95 || Lean.Name.isInternalOrNum p)
• Lean.Name.isInternalOrNum (Lean.Name.num pre i) = true
• Lean.Name.isInternalOrNum x = false

def Lean.Name.isInternalDetail : Lean.Name → Bool

Returns true if this a part of name that is internal or dynamically generated so that it may easily be changed.

Generally, user code should not explicitly use internal names.

Equations

• One or more equations did not get rendered due to their size.