# Documentation

Std.Lean.Meta.UnusedNames

Result type of Lean.Name.matchUpToIndexSuffix. See there for details.

Instances For

Succeeds if n is equal to query, except n may have an additional _i suffix for some natural number i. More specifically:

• If n = query, the result is exactMatch.
• If n = query ++ "_i" for some natural number i, the result is suffixMatch i.
• Otherwise the result is noMatch.
Equations
• One or more equations did not get rendered due to their size.

Obtain the least natural number i such that suggestion ++ "_i" is an unused name in the given local context. If suggestion itself is unused, the result is none.

Equations
• One or more equations did not get rendered due to their size.
@[inline]

Auxiliary definition for getUnusedUserNameIndex.

Equations

Obtain a name n such that n is unused in the given local context and suggestion is a prefix of n. This is similar to getUnusedName but uses a different algorithm which may or may not be faster.

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

Obtain n distinct names such that each name is unused in the given local context and suggestion is a prefix of each name.

Equations
• One or more equations did not get rendered due to their size.
def Lean.LocalContext.getUnusedUserNames.loop (suggestion : Lean.Name) (acc : ) (n : Nat) (i : Nat) :

Auxiliary definition for getUnusedUserNames.

Equations
def Lean.Meta.getUnusedUserName {m : } [inst : ] [inst : ] (suggestion : Lean.Name) :

Obtain a name n such that n is unused in the current local context and suggestion is a prefix of n.

Equations
def Lean.Meta.getUnusedUserNames {m : } [inst : ] [inst : ] (n : Nat) (suggestion : Lean.Name) :
m ()

Obtain n distinct names such that each name is unused in the current local context and suggestion is a prefix of each name.

Equations