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.
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 isexactMatch
. - If
n = query ++ "_i"
for some natural numberi
, the result issuffixMatch 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
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
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)