Documentation

Lean.ResolveName

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.

@[inline, reducible]
Equations
Instances For
    @[inline, reducible]
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[export lean_add_alias]

        Add alias a for e

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Global name resolution #

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                Instances For

                  Namespace resolution #

                  Equations
                  Instances For

                    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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Instances
                        Equations

                        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
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Given a name n, return a list of possible interpretations for global constants.

                                Similar to resolveGlobalName, but discard any candidate whose fieldList is not empty. For identifiers taken from syntax, use resolveGlobalConst instead, which respects preresolved names.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

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

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Interpret the syntax n as an identifier for a global constant, and return 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.

                                    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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Interpret 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.

                                        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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For