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.

Equations

• One or more equations did not get rendered due to their size.
• n.matchUpToIndexSuffix query = if (n == query) = true then Lean.Name.MatchUpToIndexSuffix.exactMatch else Lean.Name.MatchUpToIndexSuffix.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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• Lean.Meta.getUnusedUserName suggestion = do let __do_lift ← Lean.getLCtx pure (__do_lift.getUnusedUserName suggestion)

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.

Equations

• Lean.Meta.getUnusedUserNames n suggestion = do let __do_lift ← Lean.getLCtx pure (__do_lift.getUnusedUserNames n suggestion)