Enum SurfaceDecl 

pub enum SurfaceDecl {
    Notation {
        pattern: String,
        template: String,
        precedence: Option<u32>,
        assoc: Assoc,
        operator_form: Option<OperatorForm>,
    },
    Macro {
        pattern: String,
        template: String,
    },
    OpenSection(Option<String>),
    CloseSection(Option<String>),
    OpenNamespace(Name),
}

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.

Variants

Notation

Notation "a ⊕ b" := ((myOp a) b). and the fixity spellings, which are the same thing with the shape and associativity given by the command word instead of by the pattern.

Fields

pattern: String

template: String

precedence: Option<u32>

assoc: Assoc

operator_form: Option<OperatorForm>

For Infixl/Infixr/Prefix/Postfix, the operator’s own spelling: the pattern is just the token and the holes are implied.

Macro

Macro "twiceIt $e" := … / MacroRules "nested![$x, $xs]" := ….

Fields

pattern: String

template: String

OpenSection(Option<String>)

Section First. — or a bare Section., which is Lean’s ANONYMOUS section (section with no name), the ordinary way to scope a local without inventing a label for it. None is that form.

CloseSection(Option<String>)

End First. — and, when the innermost open scope is a NAMESPACE of that name, the close of that namespace instead. Lean spells both with one keyword and decides by what is open; deciding it here rather than in the parser is what lets the parser stay text-only.

None is the bare End. that closes an anonymous section. It closes ONLY an anonymous one: lean 4.14.0 answers namespace N … end with invalid 'end', name is missing (expected N), and a bare End that silently closed a named scope would leave every later declaration somewhere nobody wrote.

OpenNamespace(Name)

Namespace Outer.Inner. — a namespace declarations are written INTO and short names resolve against. Nothing is declared: like every other surface declaration this changes how a name is spelled and read, never what exists.

Trait Implementations

impl Clone for SurfaceDecl

fn clone(&self) -> SurfaceDecl

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SurfaceDecl

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.