Documentation

Batteries.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
    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
            Instances For

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

              Equations
              Instances For
                def Lean.Meta.getUnusedUserNames {m : TypeType} [Monad m] [Lean.MonadLCtx m] (n : Nat) (suggestion : 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
                Instances For