instance Lean.instCoeStringName : Coe String Lake.Name

@[export lean_name_hash_exported]

def Lean.Name.hashEx : Lake.Name → UInt64

def Lean.Name.getPrefix : Lake.Name → Lake.Name

def Lean.Name.getString! : Lake.Name → String

def Lean.Name.getNumParts : Lake.Name → Nat

Equations

• Lean.Name.getNumParts Lean.Name.anonymous = 0
• Lean.Name.getNumParts (Lean.Name.str p str) = Lean.Name.getNumParts p + 1
• Lean.Name.getNumParts (Lean.Name.num p i) = Lean.Name.getNumParts p + 1

def Lean.Name.updatePrefix : Lake.Name → Lake.Name → Lake.Name

def Lean.Name.componentsRev : Lake.Name → List Lake.Name

Equations

• Lean.Name.componentsRev Lean.Name.anonymous = []
• Lean.Name.componentsRev (Lean.Name.str p str) = Lean.Name.mkStr Lean.Name.anonymous str :: Lean.Name.componentsRev p
• Lean.Name.componentsRev (Lean.Name.num p i) = Lean.Name.mkNum Lean.Name.anonymous i :: Lean.Name.componentsRev p

def Lean.Name.components (n : Lake.Name) : List Lake.Name

def Lean.Name.eqStr : Lake.Name → String → Bool

def Lean.Name.isPrefixOf : Lake.Name → Lake.Name → Bool

Equations

• Lean.Name.isPrefixOf x Lean.Name.anonymous = (x == Lean.Name.anonymous)
• Lean.Name.isPrefixOf x (Lean.Name.num p' i) = (x == Lean.Name.num p' i || Lean.Name.isPrefixOf x p')
• Lean.Name.isPrefixOf x (Lean.Name.str p' str) = (x == Lean.Name.str p' str || Lean.Name.isPrefixOf x p')

def Lean.Name.isSuffixOf : Lake.Name → Lake.Name → Bool

Equations

• Lean.Name.isSuffixOf Lean.Name.anonymous x = true
• Lean.Name.isSuffixOf (Lean.Name.str p₁ s₁) (Lean.Name.str p₂ s₂) = (s₁ == s₂ && Lean.Name.isSuffixOf p₁ p₂)
• Lean.Name.isSuffixOf (Lean.Name.num p₁ n₁) (Lean.Name.num p₂ n₂) = (n₁ == n₂ && Lean.Name.isSuffixOf p₁ p₂)
• Lean.Name.isSuffixOf x x = false

def Lean.Name.cmp : Lake.Name → Lake.Name → Ordering

Equations

• Lean.Name.cmp Lean.Name.anonymous Lean.Name.anonymous = Ordering.eq
• Lean.Name.cmp Lean.Name.anonymous x = Ordering.lt
• Lean.Name.cmp x Lean.Name.anonymous = Ordering.gt
• Lean.Name.cmp (Lean.Name.num p₁ i₁) (Lean.Name.num p₂ i₂) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare i₁ i₂ | ord => ord
• Lean.Name.cmp (Lean.Name.num pre i) (Lean.Name.str pre_1 str) = Ordering.lt
• Lean.Name.cmp (Lean.Name.str pre str) (Lean.Name.num pre_1 i) = Ordering.gt
• Lean.Name.cmp (Lean.Name.str p₁ n₁) (Lean.Name.str p₂ n₂) = match Lean.Name.cmp p₁ p₂ with | Ordering.eq => compare n₁ n₂ | ord => ord

def Lean.Name.lt (x : Lake.Name) (y : Lake.Name) : Bool

def Lean.Name.quickCmpAux : Lake.Name → Lake.Name → Ordering

Equations

• Lean.Name.quickCmpAux Lean.Name.anonymous Lean.Name.anonymous = Ordering.eq
• Lean.Name.quickCmpAux Lean.Name.anonymous x = Ordering.lt
• Lean.Name.quickCmpAux x Lean.Name.anonymous = Ordering.gt
• Lean.Name.quickCmpAux (Lean.Name.num p₁ i₁) (Lean.Name.num p₂ i₂) = match compare i₁ i₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord
• Lean.Name.quickCmpAux (Lean.Name.num pre i) (Lean.Name.str pre_1 str) = Ordering.lt
• Lean.Name.quickCmpAux (Lean.Name.str pre str) (Lean.Name.num pre_1 i) = Ordering.gt
• Lean.Name.quickCmpAux (Lean.Name.str p₁ n₁) (Lean.Name.str p₂ n₂) = match compare n₁ n₂ with | Ordering.eq => Lean.Name.quickCmpAux p₁ p₂ | ord => ord

def Lean.Name.quickCmp (n₁ : Lake.Name) (n₂ : Lake.Name) : Ordering

def Lean.Name.quickLt (n₁ : Lake.Name) (n₂ : Lake.Name) : Bool

def Lean.Name.isInternal : Lake.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.isInternal (Lean.Name.str p s) = (String.get s 0 == Char.ofNat 95 || Lean.Name.isInternal p)
• Lean.Name.isInternal (Lean.Name.num p i) = Lean.Name.isInternal p
• Lean.Name.isInternal x = false

def Lean.Name.isImplementationDetail : Lake.Name → Bool

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

Implementation-detail hypothesis names start with a double underscore.

Equations

• Lean.Name.isImplementationDetail (Lean.Name.str Lean.Name.anonymous s) = String.startsWith s "__"
• Lean.Name.isImplementationDetail (Lean.Name.num p i) = Lean.Name.isImplementationDetail p
• Lean.Name.isImplementationDetail (Lean.Name.str p str) = Lean.Name.isImplementationDetail p
• Lean.Name.isImplementationDetail Lean.Name.anonymous = false

def Lean.Name.isAtomic : Lake.Name → Bool

def Lean.Name.isAnonymous : Lake.Name → Bool

def Lean.Name.isStr : Lake.Name → Bool

def Lean.Name.isNum : Lake.Name → Bool

def Lean.Name.anyS (n : Lake.Name) (f : String → Bool) : Bool

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

• Lean.Name.anyS (Lean.Name.str p s) f = (f s || Lean.Name.anyS p f)
• Lean.Name.anyS (Lean.Name.num p i) f = Lean.Name.anyS p f
• Lean.Name.anyS n f = false