Module surface 

The SURFACE environment — user-declared notation, fixity and macros.

A mathematician coins notation constantly, and the vernacular had exactly ONE infix table, hard-coded, with no extension point. This module is that extension point, and the shape of it is the whole design:

• A parser-extension command declares into the SURFACE, never into the namespace. The kernel context holds declarations; this holds ways of spelling them. Notation "a ⊕ b" := … adds no global — not the token, not the command word — because a flat namespace with one phantom per notation is a collision waiting to happen.
• Two stages, because they are two different things. A macro is a PATTERN REWRITE and can be recursive, so it runs as a source-to-source pre-pass to a fixpoint. A notation is a fixed shape with a PRECEDENCE, so it is a layer in the term parser. Lean stages them the same way and for the same reason.
• Scope is the section stack. A declaration lives in the innermost open section and dies with it, so one token can mean two things in two sections without either shadowing the other. Local is the explicit spelling of what already happens.
• A namespace is the purest case of “a spelling, not a declaration”. Namespace/End/Open change which constant a short name DENOTES and add nothing to the context. Lean agrees: its kernel Environment maps absolute names to constants and the namespace scope lives in the elaborator, with resolveGlobalName running to completion before anything reaches the kernel. So it lives here and the resolution runs in the Repl, which is why the kernel can stay a flat map of absolute keys and know nothing about any of it.
• Hygiene is not optional. A template’s own binders are renamed to names that do not occur anywhere in the expansion before its arguments are spliced in, so a template binder can never capture a call-site name. Without it Macro "twiceIt $e" := (fun x : Int => … $e …) applied at a call site that also binds x computes a silently wrong answer — not a type error.

Structs

Env

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.

Name

A hierarchical name — Lean’s Name, which is a LIST of components and not a string with dots.

Namespaces

The namespace scope: what is CURRENT, and what is OPEN.

OpenClause

One open clause: a namespace, and WHICH of its names it brings in, under WHICH spelling.

ScopeMark

Where a scope stood, so a scoped Open … in … (or a declaration’s own implicit namespace) can be wound back EXACTLY, without knowing what it pushed.

Surface

The surface environment: a stack of scopes, innermost last.

Enums

Assoc

Which way a chain of one operator nests.

OperatorForm

The shape a fixity command implies for its operator.

Resolution

What a written name denotes, once the scope has had its say.

SurfaceDecl

A declaration that extends the SURFACE rather than the context. Emitted by the command parser, applied by the REPL — so the one place a parser extension can land is the surface environment.

Constants

ANONYMOUS_SECTION

How an ANONYMOUS section is named in a report. Lean’s section may be written with no name at all, and a scope with no name still has to be reportable — as an unclosed scope at the end of a document, and as the scope a mismatched End failed to close.

ROOT_ESCAPE

The one name that is never relative: _root_.x is the absolute x, whatever is open.

Functions

fill_defaults

Fill every OMITTED DEFAULT ARGUMENT in term, at every application spine in it.

resolve_names

resolve_names_in against an environment that is only its declared keys — known — and shadows nothing.

resolve_names_in

Resolve every global name written in term against the scope, BEFORE any elaboration sees it — Lean’s staging, and the whole content of “name resolution completes before translation begins”.

respell_names

The inverse of resolve_names_in, for a term already in KEY space: every global is re-spelled so that resolving the result in this same scope reaches exactly the key it holds now.