Enum BinderKind 

pub enum BinderKind {
    Explicit,
    Implicit,
    StrictImplicit,
    Instance,
}

How a parameter is SUPPLIED at a call site – Lean’s four binder kinds.

The kernel has exactly one Pi, so a binder kind is not a typing distinction: {A : Type} -> A and (A : Type) -> A and ⦃A : Type⦄ -> A denote the same type and the same terms inhabit it. What differs is what the ELABORATOR does at an application, and that is why the kind must travel out of the parser beside the term rather than inside it.

Variants

Explicit

(x : T) – the caller writes the argument.

Implicit

{x : T} – inserted eagerly, solved by unification.

StrictImplicit

⦃x : T⦄ (Lean’s strict-implicit brackets) – inserted only when a LATER explicit argument is actually supplied, so an unapplied nilOf stays the polymorphic function rather than becoming an application with an unsolvable metavariable in it.

Instance

[C x] – resolved from the instance database, after the explicit arguments have pinned the class’s type variables.

Implementations

impl BinderKind

pub fn as_param_kind(self) -> ParamKind

The elaborator’s ParamKind for this binder – now a BIJECTION, one variant each.

★ THE LOSSY STEP IS GONE, AND THIS WAS THE ONE LINE. ParamKind had three variants and this enum four, so a strict implicit could only be collapsed onto Implicit. The collapse was made HERE, in one named function, rather than spelled at each hand-over site, against the day ParamKind grew its fourth variant. It has – Lean’s BinderInfo has exactly four constructors (Lean/Expr.lean:69) and ⦃⦄ earns its own because App.lean:726’s processStrictImplicitArg gives it a rule no other kind has: insert only if (← hasArgsToProcess), otherwise finalize. ParamKind::StrictImplicit now exists and elaborate_app_against implements precisely that rule, so ⦃α⦄ reaches the elaborator as itself and this function is a BIJECTION with no information left to lose. lean_conformance_t05_elaboration::a_strict_implicit_is_not_instantiated_until_an_explicit_argument_follows is what pins the behaviour end to end.

The legacy implicit_count model still STOPS at a strict implicit (count_implicits): a count can only describe an unconditional prefix, and over-inserting there emits a metavariable nothing can solve.

pub fn of_param_kind(kind: ParamKind) -> BinderKind

The binder kind for an elaborator ParamKind – the inverse of as_param_kind.

Trait Implementations

impl Clone for BinderKind

fn clone(&self) -> BinderKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BinderKind

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

Formats the value using the given formatter.

impl Hash for BinderKind

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for BinderKind

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

impl Eq for BinderKind

impl StructuralPartialEq for BinderKind