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.

source
def Lean.throwReservedNameNotAvailable {m : Type → Type} [Monad m] [MonadError m] (declName reservedName : Name) :
m Unit
Equations

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

Instances For

source
def Lean.ensureReservedNameAvailable {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (suffix : String) :
m Unit
Equations

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

Instances For

source
opaque Lean.reservedNamePredicatesRef :
IO.Ref (Array (Environment → Name → Bool))

Global reference containing all reserved name predicates.

source
def Lean.registerReservedNamePredicate (p : Environment → Name → Bool) :
IO Unit

Registers a new reserved name predicate.

Equations

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

Instances For

source
opaque Lean.reservedNamePredicatesExt :
EnvExtension (Array (Environment → Name → Bool))
source
@[export lean_is_reserved_name]
def Lean.isReservedName (env : Environment) (name : Name) :
Bool

Returns `true` if `name` is a reserved name.

Equations

- Lean.isReservedName env name = (Lean.reservedNamePredicatesExt.getState env).any fun (x : Lean.Environment → Lean.Name → Bool) => x env name

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

source
@[reducible, inline]
abbrev Lean.AliasState :
Type
Equations

- Lean.AliasState = Lean.SMap Lean.Name (List Lean.Name)

Instances For

source
@[reducible, inline]
abbrev Lean.AliasEntry :
Type
Equations

- Lean.AliasEntry = (Lean.Name × Lean.Name)

Instances For

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

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

Instances For

source
opaque Lean.aliasExtension :
SimplePersistentEnvExtension AliasEntry AliasState
source
@[export lean_add_alias]
def Lean.addAlias (env : Environment) (a e : Name) :
Environment

Add alias `a` for `e`

Equations

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

Instances For

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

- Lean.getAliasState env = Lean.aliasExtension.getState env

Instances For

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

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

Equations

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

Instances For

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

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

Instances For

# Global name resolution #

source
opaque Lean.ResolveName.backward.privateInPublic :
Lean.Option Bool
source
opaque Lean.ResolveName.backward.privateInPublic.warn :
Lean.Option Bool
source
def Lean.ResolveName.resolveGlobalName (env : Environment) (opts : Options) (ns : Name) (openDecls : List OpenDecl) (id : Name) :
List (Name × List String)

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

- Lean.ResolveName.resolveGlobalName env opts ns openDecls id = Lean.ResolveName.resolveGlobalName.loop✝ env opts ns openDecls (Lean.extractMacroScopes id) (Lean.extractMacroScopes id).name []

Instances For

# Namespace resolution #

source
def Lean.ResolveName.resolveNamespaceUsingScope? (env : Environment) (n ns : Name) :
Option Name
Equations

- One or more equations did not get rendered due to their size.
- Lean.ResolveName.resolveNamespaceUsingScope? env n (p.str str) = if env.isNamespace (p.str str ++ n) = true then some (p.str str ++ n) else Lean.ResolveName.resolveNamespaceUsingScope? env n p
- Lean.ResolveName.resolveNamespaceUsingScope? env n ns = panicWithPosWithDecl "Lean.ResolveName" "Lean.ResolveName.resolveNamespaceUsingScope?" 230 9 "unreachable code has been reached"

Instances For

source
def Lean.ResolveName.resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) :
List OpenDecl → List 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

Instances For

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

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

Instances For

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

- getCurrNamespace : m Name
- getOpenDecls : m (List OpenDecl)

Instances

source
instance Lean.instMonadResolveNameOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadResolveName m] :
MonadResolveName n
Equations

- Lean.instMonadResolveNameOfMonadLift m n = { getCurrNamespace := liftM Lean.getCurrNamespace, getOpenDecls := liftM Lean.getOpenDecls }

source
def Lean.checkPrivateInPublic {m : Type → Type} [Monad m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (id : Name) :
m Unit
Equations

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

Instances For

source
def Lean.isInaccessiblePrivateName {m : Type → Type} [MonadLog m] [AddMessageContext m] [Monad m] [MonadEnv m] [MonadOptions m] (n : Name) :
m Bool
Equations

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

Instances For

source
def Lean.resolveGlobalName {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (id : Name) (enableLog : Bool := true) :
m (List (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])]`

If `enableLog` is false, this function does not ever log warnings etc, which is useful if it may be called incidentally or multiple times.

Equations

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

Instances For

source
def Lean.resolveNamespaceCore {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) (allowEmpty : Bool := false) :
m (List 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.

Instances For

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

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

Equations

- One or more equations did not get rendered due to their size.
- Lean.resolveNamespace x✝ = Lean.throwErrorAt x✝.raw ((Lean.MessageData.ofFormat ∘ Std.format) (toString "expected identifier"))

Instances For

source
def Lean.resolveUniqueNamespace {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Ident) :
m 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.

Instances For

source
def Lean.filterFieldList {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (n : Name) (cs : List (Name × List String)) :
m (List Name)

Helper function for `resolveGlobalConstCore`.

Equations

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

Instances For

source
def Lean.ensureNoOverload {m : Type → Type} [Monad m] [MonadError m] (n : Name) (cs : List Name) :
m Name

Helper function for `resolveGlobalConstNoOverloadCore`

Equations

- One or more equations did not get rendered due to their size.
- Lean.ensureNoOverload n [ns] = pure ns

Instances For

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

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

Equations

- Lean.resolveGlobalConstNoOverloadCore n = do let __do_lift ← Lean.resolveGlobalConstCore✝ n Lean.ensureNoOverload n __do_lift

Instances For

source
def Lean.preprocessSyntaxAndResolve {m : Type → Type} [Monad m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) :
m (List Name)
Equations

- One or more equations did not get rendered due to their size.
- Lean.preprocessSyntaxAndResolve stx k = Lean.throwErrorAt stx ((Lean.MessageData.ofFormat ∘ Std.format) (toString "expected identifier"))

Instances For

source
def Lean.resolveGlobalConst {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] [MonadError m] (stx : Syntax) :
m (List Name)

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

- `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

- Lean.resolveGlobalConst stx = Lean.preprocessSyntaxAndResolve stx Lean.resolveGlobalConstCore✝

Instances For

source
def Lean.ensureNonAmbiguous {m : Type → Type} [Monad m] [MonadError m] (id : Syntax) (cs : List Name) :
m 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

- One or more equations did not get rendered due to their size.
- Lean.ensureNonAmbiguous id [] = panicWithPosWithDecl "Lean.ResolveName" "Lean.ensureNonAmbiguous" 429 11 "unreachable code has been reached"
- Lean.ensureNonAmbiguous id [c] = pure c

Instances For

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

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

- `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

- Lean.resolveGlobalConstNoOverload id = do let __do_lift ← Lean.resolveGlobalConst id Lean.ensureNonAmbiguous id __do_lift

Instances For

source
def Lean.resolveLocalName {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] [MonadLCtx m] (n : Name) :
m (Option (Expr × List String))

Resolves the name `n` in the local context.

Equations

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

Instances For

source
def Lean.unresolveNameGlobal {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (n₀ : Name) (fullNames allowHorizAliases : Bool := false) (filter : Name → m Bool := fun (x : Name) => pure true) :
m Name

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.

The name `n₀` may be private.

Equations

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

Instances For

source
def Lean.unresolveNameGlobalAvoidingLocals {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] [MonadLCtx m] (n₀ : Name) (fullNames : Bool := false) :
m Name

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

Equations

- Lean.unresolveNameGlobalAvoidingLocals n₀ fullNames = Lean.unresolveNameGlobal n₀ fullNames false fun (n : Lean.Name) => Option.isNone <$> Lean.resolveLocalName n

Instances For