Documentation

Lean.Data.Name

@[export lean_name_hash_exported]
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x, x with | , s' => s == s' | x, x_1 => false
Equations
Equations
Equations
Equations
• = ()
Equations
Equations
• = match compare () () with | Ordering.eq => | ord => ord
def Lean.Name.quickLt (n₁ : Lean.Name) (n₂ : Lean.Name) :
Equations
• = ()

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

Checks whether the name is an implementation-detail hypothesis name.

Equations
Equations
• = match x with | Lean.Name.anonymous => true | => true | => true | x => false
Equations
• = match x with | Lean.Name.anonymous => true | x => false
Equations
Equations
def Lean.Name.anyS (n : Lean.Name) (f : ) :

Return true if n contains a string part s that satifies f.

Examples:

#eval (foo.bla).anyS (·.startsWith "fo") -- true
#eval (foo.bla).anyS (·.startsWith "boo") -- false

Equations
Equations