inductive Lean.Name.MatchUpToIndexSuffix : Type

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

• exactMatch : MatchUpToIndexSuffix

  Exact match.

• noMatch : MatchUpToIndexSuffix

  No match.

• suffixMatch (i : Nat) : MatchUpToIndexSuffix

  Match up to suffix.

def Lean.Name.matchUpToIndexSuffix (n query : Name) : MatchUpToIndexSuffix

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.

def Lean.LocalContext.getUnusedUserNameIndex (lctx : LocalContext) (suggestion : Name) : Option Nat

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.

@[inline]

def Lean.LocalContext.getUnusedUserNameIndex.updateMinSuffix : Option Nat → Nat → Option Nat

Auxiliary definition for getUnusedUserNameIndex.

def Lean.LocalContext.getUnusedUserName (lctx : LocalContext) (suggestion : Name) : Name

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.

def Lean.LocalContext.getUnusedUserNames (lctx : LocalContext) (n : Nat) (suggestion : Name) : Array Name

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

def Lean.LocalContext.getUnusedUserNames.loop (suggestion : Name) (acc : Array Name) (n i : Nat) : Array Name

Auxiliary definition for getUnusedUserNames.

def Lean.Meta.getUnusedUserName {m : Type → Type} [Monad m] [MonadLCtx m] (suggestion : Name) : m Name

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

def Lean.Meta.getUnusedUserNames {m : Type → Type} [Monad m] [MonadLCtx m] (n : Nat) (suggestion : Name) : m (Array Name)

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