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.

def Lean.Name.isInternalDetail.matchPrefix (s : String) (pre : String) : Bool

Check that a string begins with the given prefix, and then is only digit characters.

Equations

• Lean.Name.isInternalDetail.matchPrefix s pre = (s.startsWith pre && (s.drop pre.length).all Char.isDigit)