inductive Lean.Name.MatchUpToIndexSuffix : Type

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

• exactMatch: Lean.Name.MatchUpToIndexSuffix

  Exact match.

• noMatch: Lean.Name.MatchUpToIndexSuffix

  No match.

• suffixMatch: Nat → Lean.Name.MatchUpToIndexSuffix

  Match up to suffix.

def Lean.Name.matchUpToIndexSuffix (n query : Lean.Name) : Lean.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 : Lean.LocalContext) (suggestion : Lean.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.

@[inline]

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

Auxiliary definition for getUnusedUserNameIndex.

Equations

• Lean.LocalContext.getUnusedUserNameIndex.updateMinSuffix none x = some x
• Lean.LocalContext.getUnusedUserNameIndex.updateMinSuffix (some i) x = some (i.max x)

def Lean.LocalContext.getUnusedUserName (lctx : Lean.LocalContext) (suggestion : Lean.Name) : Lean.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 : Lean.LocalContext) (n : Nat) (suggestion : Lean.Name) : Array Lean.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.LocalContext.getUnusedUserNames.loop (suggestion : Lean.Name) (acc : Array Lean.Name) (n i : Nat) : Array Lean.Name

Auxiliary definition for getUnusedUserNames.

Equations

• Lean.LocalContext.getUnusedUserNames.loop suggestion acc 0 i = acc
• Lean.LocalContext.getUnusedUserNames.loop suggestion acc n_2.succ i = Lean.LocalContext.getUnusedUserNames.loop suggestion (acc.push (suggestion.appendIndexAfter i)) n_2 (i + 1)

def Lean.Meta.getUnusedUserName {m : Type → Type} [Monad m] [Lean.MonadLCtx m] (suggestion : Lean.Name) : m Lean.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] [Lean.MonadLCtx m] (n : Nat) (suggestion : Lean.Name) : m (Array Lean.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)