Struct Env 

pub struct Env<'e> {
    pub known: &'e dyn Fn(&str) -> bool,
    pub shadow: &'e dyn Fn(&str) -> Option<String>,
}

The environment a written name is resolved against — the two questions resolution asks of it, as closures, which is what keeps the kernel out of the surface.

Fields

known: &'e dyn Fn(&str) -> bool

Is this absolute key declared?

shadow: &'e dyn Fn(&str) -> Option<String>

The fresh identity this absolute written name denotes, when a shadow redirects it (Context::shadow_of).

Implementations

impl Env<'_>

pub fn resolve(&self, ns: &Namespaces, written: &Name) -> Resolution

What written denotes: the absolute key the namespace scope resolves it to, then — unless it was written with the _root_ escape — the identity a shadow redirects that key to.

★ THE ONE RESOLUTION POINT. Every surface that reads a name reads it here: the term and command doors through resolve_names_in, the literate door as it reads each name, the REPL’s Print Axioms, Structure and Quotient references. The shadow is applied AFTER the scope has chosen an absolute key, and to that key alone, so a shadow never takes part in the scope’s own decisions (which namespace, which open, whether two readings are ambiguous), and the escape keeps meaning what it means in Lean: the environment’s own declaration, whatever shadows its name.