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

@[inline, reducible]

abbrev Lean.AliasState : Type

Equations

• Lean.AliasState = Lean.SMap Lake.Name (List Lake.Name)

@[inline, reducible]

abbrev Lean.AliasEntry : Type

Equations

• Lean.AliasEntry = (Lake.Name × Lake.Name)

def Lean.addAliasEntry (s : Lean.AliasState) (e : Lean.AliasEntry) : Lean.AliasState

Equations

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

opaque Lean.aliasExtension : Lean.SimplePersistentEnvExtension Lean.AliasEntry Lean.AliasState

@[export lean_add_alias]

def Lean.addAlias (env : Lean.Environment) (a : Lake.Name) (e : Lake.Name) : Lean.Environment

Add alias a for e

Equations

• Lean.addAlias env a e = Lean.PersistentEnvExtension.addEntry Lean.aliasExtension env (a, e)

def Lean.getAliasState (env : Lean.Environment) : Lean.AliasState

Equations

• Lean.getAliasState env = Lean.SimplePersistentEnvExtension.getState Lean.aliasExtension env

def Lean.getAliases (env : Lean.Environment) (a : Lake.Name) (skipProtected : Bool) : List Lake.Name

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.

def Lean.getRevAliases (env : Lean.Environment) (e : Lake.Name) : List Lake.Name

Equations

• Lean.getRevAliases env e = Lean.SMap.fold (fun as a es => if List.contains es e = true then a :: as else as) [] (Lean.SimplePersistentEnvExtension.getState Lean.aliasExtension env)

Global name resolution

def Lean.ResolveName.resolveGlobalName (env : Lean.Environment) (ns : Lake.Name) (openDecls : List Lean.OpenDecl) (id : Lake.Name) : List (Lake.Name × List String)

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.ResolveName.resolveGlobalName.loop env ns openDecls extractionResult id projs = []

Namespace resolution

def Lean.ResolveName.resolveNamespaceUsingScope? (env : Lean.Environment) (n : Lake.Name) : Lake.Name → Option Lake.Name

Equations

• One or more equations did not get rendered due to their size.
• Lean.ResolveName.resolveNamespaceUsingScope? env n Lean.Name.anonymous = if Lean.Environment.isNamespace env n = true then some n else none

def Lean.ResolveName.resolveNamespaceUsingOpenDecls (env : Lean.Environment) (n : Lake.Name) : List Lean.OpenDecl → List Lake.Name

Equations

• One or more equations did not get rendered due to their size.
• Lean.ResolveName.resolveNamespaceUsingOpenDecls env n [] = []
• Lean.ResolveName.resolveNamespaceUsingOpenDecls env n (head :: ds) = Lean.ResolveName.resolveNamespaceUsingOpenDecls env n ds

def Lean.ResolveName.resolveNamespace (env : Lean.Environment) (ns : Lake.Name) (openDecls : List Lean.OpenDecl) (id : Lake.Name) : List Lake.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 extact 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.

class Lean.MonadResolveName (m : Type → Type) : Type

• getCurrNamespace : m Lake.Name
• getOpenDecls : m (List Lean.OpenDecl)

instance Lean.instMonadResolveName (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.MonadResolveName m] : Lean.MonadResolveName n

Equations

• Lean.instMonadResolveName m n = { getCurrNamespace := liftM Lean.getCurrNamespace, getOpenDecls := liftM Lean.getOpenDecls }

def Lean.resolveGlobalName {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] (id : Lake.Name) : m (List (Lake.Name × List String))

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

• resolveGlobalName x => [(Foo.x, [])]
• resolveGlobalName x.y => [(Foo.x.y, [])]
• resolveGlobalName x.z.w => [(Foo.x, [z, w])]

After open Foo open Boo, we have

• resolveGlobalName x => [(Foo.x, []), (Boo.x, [])]
• resolveGlobalName x.y => [(Foo.x.y, [])]
• resolveGlobalName x.z.w => [(Foo.x, [z, w]), (Boo.x, [z, w])]

Equations

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

def Lean.resolveNamespaceCore {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] (id : Lake.Name) (allowEmpty : optParam Bool false) : m (List Lake.Name)

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.

def Lean.resolveNamespace {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] : Lean.Ident → m (List Lake.Name)

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

Equations

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

def Lean.resolveUniqueNamespace {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] (id : Lean.Ident) : m Lake.Name

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

Equations

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

def Lean.resolveGlobalConstCore {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] (n : Lake.Name) : m (List Lake.Name)

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.

def Lean.resolveGlobalConstNoOverloadCore {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] (n : Lake.Name) : m Lake.Name

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.

def Lean.resolveGlobalConst {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] : Lean.Syntax → m (List Lake.Name)

Interpret the syntax n as an identifier for a global constant, and return a list of resolved constant names that it could be refering 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

• resolveGlobalConst x => [Foo.x]
• resolveGlobalConst x.y => [Foo.x.y]
• resolveGlobalConst x.z.w => error: unknown constant

After open Foo open Boo, we have

• resolveGlobalConst x => [Foo.x, Boo.x]
• resolveGlobalConst x.y => [Foo.x.y]
• resolveGlobalConst x.z.w => error: unknown constant

Equations

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

def Lean.resolveGlobalConstNoOverload {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] [Lean.MonadError m] (id : Lean.Syntax) : m Lake.Name

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

• resolveGlobalConstNoOverload x => Foo.x
• resolveGlobalConstNoOverload x.y => Foo.x.y
• resolveGlobalConstNoOverload x.z.w => error: unknown constant

After open Foo open Boo, we have

• resolveGlobalConstNoOverload x => error: ambiguous identifier
• resolveGlobalConstNoOverload x.y => Foo.x.y
• resolveGlobalConstNoOverload x.z.w => error: unknown constant

Equations

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

def Lean.unresolveNameGlobal {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] (n₀ : Lake.Name) (fullNames : optParam Bool false) : m Lake.Name

Equations

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

def Lean.unresolveNameGlobal.unresolveNameCore {m : Type → Type} [Monad m] [Lean.MonadResolveName m] [Lean.MonadEnv m] (n₀ : Lake.Name) (n : Lake.Name) : m (Option Lake.Name)

Equations

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