Documentation

Lean.ResolveName

Reserved names.

We use reserved names for automatically generated theorems (e.g., equational theorems). Automation may register new reserved name predicates. In this module, we just check the registered predicates, but do not trigger actions associated with them. For example, give a definition foo, we flag foo.def as reserved symbol.

def Lean.throwReservedNameNotAvailable {m : TypeType} [Monad m] [MonadError m] (declName reservedName : Name) :
Equations
    Instances For
      def Lean.ensureReservedNameAvailable {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (suffix : String) :
      Equations
        Instances For

          Global reference containing all reserved name predicates.

          Registers a new reserved name predicate.

          Equations
            Instances For
              @[export lean_is_reserved_name]

              Returns true if name is a reserved name.

              Equations
                Instances For

                  We use aliases to implement the export <id> (<id>+) command. An export A (x) in the namespace B produces an alias B.x ~> A.x.

                  @[reducible, inline]
                  Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For
                          Equations
                            Instances For
                              @[export lean_add_alias]

                              Add alias a for e

                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      def Lean.getAliases (env : Environment) (a : Name) (skipProtected : Bool) :

                                      Retrieve aliases for a. If skipProtected is true, then the resulting list only includes declarations that are not marked as protected.

                                      Equations
                                        Instances For
                                          Equations
                                            Instances For

                                              Global name resolution #

                                              Primitive global name resolution procedure. It does not trigger actions associated with reserved names. Recall that Lean has reserved names. For example, a definition foo has a reserved name foo.def for theorem containing stating that foo is equal to its definition. The action associated with foo.def automatically proves the theorem. At the macro level, the name is resolved, but the action is not executed.

                                              Equations
                                                Instances For
                                                  def Lean.ResolveName.resolveGlobalName.loop (env : Environment) (ns : Name) (openDecls : List OpenDecl) (extractionResult : MacroScopesView) (id : Name) (projs : List String) :
                                                  Equations
                                                    Instances For

                                                      Namespace resolution #

                                                      def Lean.ResolveName.resolveNamespace (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) :

                                                      Given a name id try to find namespaces it may refer to. The resolution procedure works as follows

                                                      1- If id is in the scope of namespace commands the namespace s_1. ... . s_n, then we include s_1 . ... . s_i ++ n in the result if it is the name of an existing namespace. We search "backwards", and include at most one of the in the list of resulting namespaces.

                                                      2- If id is the exact name of an existing namespace, then include id

                                                      3- Finally, for each command open N, include in the result N ++ n if it is the name of an existing namespace. We only consider simple open commands.

                                                      Equations
                                                        Instances For
                                                          Instances

                                                            Given a name n, return a list of possible interpretations. Each interpretation is a pair (declName, fieldList), where declName is the name of a declaration in the current environment, and fieldList are (potential) field names. The pair is needed because in Lean . may be part of a qualified name or a field (aka dot-notation). As an example, consider the following definitions

                                                            def Boo.x   := 1
                                                            def Foo.x   := 2
                                                            def Foo.x.y := 3
                                                            

                                                            After open Foo, we have

                                                            After open Foo open Boo, we have

                                                            Equations
                                                              Instances For
                                                                def Lean.resolveNamespaceCore {m : TypeType} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) (allowEmpty : Bool := false) :

                                                                Given a namespace name, return a list of possible interpretations. Names extracted from syntax should be passed to resolveNamespace instead.

                                                                Equations
                                                                  Instances For

                                                                    Given a namespace identifier, return a list of possible interpretations.

                                                                    Equations
                                                                      Instances For

                                                                        Given a namespace identifier, return the unique interpretation or else fail.

                                                                        Equations
                                                                          Instances For
                                                                            def Lean.filterFieldList {m : TypeType} [Monad m] [MonadError m] (n : Name) (cs : List (Name × List String)) :

                                                                            Helper function for resolveGlobalConstCore.

                                                                            Equations
                                                                              Instances For
                                                                                def Lean.ensureNoOverload {m : TypeType} [Monad m] [MonadError m] (n : Name) (cs : List Name) :

                                                                                Helper function for resolveGlobalConstNoOverloadCore

                                                                                Equations
                                                                                  Instances For

                                                                                    For identifiers taken from syntax, use resolveGlobalConstNoOverload instead, which respects preresolved names.

                                                                                    Equations
                                                                                      Instances For
                                                                                        def Lean.preprocessSyntaxAndResolve {m : TypeType} [Monad m] [MonadError m] (stx : Syntax) (k : Namem (List Name)) :
                                                                                        Equations
                                                                                          Instances For

                                                                                            Interprets the syntax n as an identifier for a global constant, and returns a list of resolved constant names that it could be referring to based on the currently open namespaces. This should be used instead of resolveGlobalConstCore for identifiers taken from syntax because Syntax objects may have names that have already been resolved.

                                                                                            Consider using realizeGlobalConst if you need to handle reserved names, and realizeGlobalConstWithInfo if you want the syntax to show the resulting name's info on hover.

                                                                                            Example: #

                                                                                            def Boo.x   := 1
                                                                                            def Foo.x   := 2
                                                                                            def Foo.x.y := 3
                                                                                            

                                                                                            After open Foo, we have

                                                                                            After open Foo open Boo, we have

                                                                                            Equations
                                                                                              Instances For
                                                                                                def Lean.ensureNonAmbiguous {m : TypeType} [Monad m] [MonadError m] (id : Syntax) (cs : List Name) :

                                                                                                Given a list of names produced by resolveGlobalConst, throws an error if the list does not contain exactly one element. Recall that resolveGlobalConst does not return empty lists.

                                                                                                Equations
                                                                                                  Instances For

                                                                                                    Interprets the syntax n as an identifier for a global constant, and return a resolved constant name. If there are multiple possible interpretations it will throw.

                                                                                                    Consider using realizeGlobalConstNoOverload if you need to handle reserved names, and realizeGlobalConstNoOverloadWithInfo if you want the syntax to show the resulting name's info on hover.

                                                                                                    Example: #

                                                                                                    def Boo.x   := 1
                                                                                                    def Foo.x   := 2
                                                                                                    def Foo.x.y := 3
                                                                                                    

                                                                                                    After open Foo, we have

                                                                                                    After open Foo open Boo, we have

                                                                                                    Equations
                                                                                                      Instances For

                                                                                                        Resolves the name n in the local context.

                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            def Lean.resolveLocalName.go (localDecl : LocalDecl) (givenNameView : MacroScopesView) (fullDeclName ns : Name) :
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                def Lean.resolveLocalName.loop {m : TypeType} [Monad m] [MonadResolveName m] [MonadEnv m] (view : MacroScopesView) (findLocalDecl? : MacroScopesViewBoolOption LocalDecl) (n : Name) (projs : List String) (globalDeclFound : Bool) :
                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    def Lean.unresolveNameGlobal {m : TypeType} [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames allowHorizAliases : Bool := false) (filter : Namem Bool := fun (x : Name) => pure true) :

                                                                                                                    Finds a name that unambiguously resolves to the given name n₀. Considers suffixes of n₀ and suffixes of aliases of n₀ when "unresolving". Aliases are considered first.

                                                                                                                    When fullNames is true, returns either n₀ or _root_.n₀.

                                                                                                                    When allowHorizAliases is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out. The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name). "Non-API exports" arise from (1) using export to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.

                                                                                                                    filter specifies a predicate that the unresolved name must additionally satisfy.

                                                                                                                    This function is meant to be used for pretty printing. If n₀ is an accessible name, then the result will be an accessible name.

                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        def Lean.unresolveNameGlobal.unresolveNameCore {m : TypeType} [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (filter : Namem Bool := fun (x : Name) => pure true) (n : Name) :
                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            def Lean.unresolveNameGlobalAvoidingLocals {m : TypeType} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n₀ : Name) (fullNames : Bool := false) :

                                                                                                                            Like Lean.unresolveNameGlobal, but also ensures that the unresolved name does not conflict with the names of any local declarations.

                                                                                                                            Equations
                                                                                                                              Instances For