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
          Instances For
            @[inline]

            Auxiliary definition for getUnusedUserNameIndex.

            Equations
              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
                  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
                      Instances For

                        Auxiliary definition for getUnusedUserNames.

                        Equations
                          Instances For
                            def Lean.Meta.getUnusedUserName {m : TypeType} [Monad m] [MonadLCtx m] (suggestion : Name) :

                            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] [MonadLCtx m] (n : Nat) (suggestion : 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