Struct DeclarationSurface 

pub struct DeclarationSurface {
    pub kernel_type: Term,
    pub binders: Vec<BinderSurface>,
}

A declared type split into the pure kernel type the context is keyed at and the per-parameter surface information that has to be recorded beside it.

★ ONE CALL AT THE DECLARATION DOOR. Before this, the declaration door read a (Term, usize) pair and there was nowhere for a default, an auto-param or a non-leading implicit to go – so Definition f : Int -> (m : Int := 3) -> Int registered a type with a reserved marker still inside it, which the kernel then refused as an unbound global. Every piece of surface-only information now leaves the parser through this one struct.

Fields

kernel_type: Term

The declared type with every binder marker stripped: what Context is keyed at.

binders: Vec<BinderSurface>

One entry per binder of the type’s top-level telescope, outermost first.

Implementations

impl DeclarationSurface

pub fn param_kinds(&self) -> Vec<ParamKind>

The elaborator’s parameter kinds, one per telescope position.

pub fn leading_implicits(&self) -> usize

How many LEADING implicit parameters the declaration has – the legacy count model, and exactly the number TermParser::parse_with_implicits reports.

pub fn needs_recording(&self) -> bool

Does any binder carry surface information the plain (Term, usize) door would lose? A declaration for which this is false can be registered exactly as it always was.

Trait Implementations

impl Clone for DeclarationSurface

fn clone(&self) -> DeclarationSurface

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DeclarationSurface

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

Formats the value using the given formatter.

impl PartialEq for DeclarationSurface

fn eq(&self, other: &DeclarationSurface) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for DeclarationSurface