Additional functions on Lean.Name.

We provide allNames and allNamesByModule, as well as assorted utilities on Name such as mapPrefix, fromComponents, splitAt and isPrefixOf?.

def allNames (p : Lean.Name → Bool) : Lean.CoreM (Array Lean.Name)

Retrieve all names in the environment satisfying a predicate.

Equations

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

def allNamesByModule (p : Lean.Name → Bool) : Lean.CoreM (Std.HashMap Lean.Name (Array Lean.Name))

Retrieve all names in the environment satisfying a predicate, gathered together into a HashMap according to the module they are defined in.

Equations

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

def Lean.Name.willRoundTrip (n : Name) : Bool

Determines if the pretty-printed version of the given name would parse as an ident with an underlying name (via getId) equal to the original name. The pretty-printer usually escapes unparsable components of a name with «», but makes exceptions for various names with special meaning, meaning that the result does not round trip. We therefore re-check those conditions here.

This function is intended to be "safe" in that if it returns true, the name will definitely round trip. (The converse is not guaranteed.) Any deviation from this behavior is a bug which should be fixed.

Equations

• n.willRoundTrip = (!n.isAnonymous && !n.hasMacroScopes && !Lean.Name.willRoundTrip.maybePseudoSyntax✝ n && !n.isInaccessibleUserName && Lean.Name.willRoundTrip.go✝ n)

def Lean.Name.isBlackListed {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

Equations

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

def Lean.Name.decapitalize (n : Name) : Name

Decapitalize the last component of a name.

Equations

• n.decapitalize = n.modifyBase fun (x : Lean.Name) => match x with | p.str s => p.str s.decapitalize | n => n

@[specialize #[]]

def Lean.Name.mapPrefix (f : Name → Option Name) (n : Name) : Name

Find the largest prefix n of a Name such that f n != none, then replace this prefix with the value of f n.

Equations

• Lean.Name.mapPrefix f Lean.Name.anonymous = (match f Lean.Name.anonymous with | some n' => pure n' | x => Lean.Name.anonymous).run
• Lean.Name.mapPrefix f (n'.str s) = (match f (n'.str s) with | some n' => pure n' | x => (Lean.Name.mapPrefix f n').mkStr s).run
• Lean.Name.mapPrefix f (n'.num i) = (match f (n'.num i) with | some n' => pure n' | x => (Lean.Name.mapPrefix f n').mkNum i).run

def Lean.Name.fromComponents : List Name → Name

Build a name from components. For example, from_components [`foo, `bar] becomes `foo.bar. It is the inverse of Name.components on list of names that have single components.

Equations

• Lean.Name.fromComponents = Lean.Name.fromComponents.go✝ Lean.Name.anonymous

def Lean.Name.updateLast (f : String → String) : Name → Name

Update the last component of a name.

Equations

• Lean.Name.updateLast f (pre.str s) = pre.str (f s)
• Lean.Name.updateLast f x✝ = x✝

def Lean.Name.lastComponentAsString : Name → String

Get the last field of a name as a string. Doesn't raise an error when the last component is a numeric field.

Equations

• (n.str s).lastComponentAsString = s
• (pre.num i).lastComponentAsString = toString i
• Lean.Name.anonymous.lastComponentAsString = ""

def Lean.Name.splitAt (nm : Name) (n : Nat) : Name × Name

nm.splitAt n splits a name nm in two parts, such that the second part has depth n, i.e. (nm.splitAt n).2.getNumParts = n (assuming nm.getNumParts ≥ n). Example: splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat).

Equations

• nm.splitAt n = match List.splitAt n nm.componentsRev with | (nm2, nm1) => (Lean.Name.fromComponents nm1.reverse, Lean.Name.fromComponents nm2.reverse)

def Lean.Name.isPrefixOf? (pre nm : Name) : Option Name

isPrefixOf? pre nm returns some post if nm = pre ++ post. Note that this includes the case where nm has multiple more namespaces. If pre is not a prefix of nm, it returns none.

Equations

• pre.isPrefixOf? Lean.Name.anonymous = if (pre == Lean.Name.anonymous) = true then some Lean.Name.anonymous else none
• pre.isPrefixOf? (p'.num a) = if (pre == p'.num a) = true then some Lean.Name.anonymous else Option.map (fun (x : Lean.Name) => x.num a) (pre.isPrefixOf? p')
• pre.isPrefixOf? (p'.str s) = if (pre == p'.str s) = true then some Lean.Name.anonymous else Option.map (fun (x : Lean.Name) => x.str s) (pre.isPrefixOf? p')