Struct BinderSurface 

pub struct BinderSurface {
    pub name: String,
    pub kind: BinderKind,
    pub declared: Term,
    pub default: Option<Term>,
    pub auto: Option<String>,
}

Everything the SURFACE says about ONE parameter that the kernel’s three-field Term::Pi cannot hold: how it is supplied, and what fills it when the caller does not.

Fields

name: String

The parameter’s name. "_" for an anonymous binder – A -> B names nothing, and TermParser::name_anonymous_binders recovers those names from the definition’s body.

kind: BinderKind

How the caller supplies it.

declared: Term

The declared type, with every marker stripped – the type the kernel sees.

default: Option<Term>

(m : T := e) – the term inlined when the caller omits this argument.

auto: Option<String>

(h : P := by tac) – the tactic that must prove declared AFRESH at each call site. Distinct from default because a default is inlined once per omission and an auto-param is a different proof term at every call site, about that call site’s own proposition.

Trait Implementations

impl Clone for BinderSurface

fn clone(&self) -> BinderSurface

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BinderSurface

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

Formats the value using the given formatter.

impl PartialEq for BinderSurface

fn eq(&self, other: &BinderSurface) -> 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 BinderSurface