Enum Annotation 

pub enum Annotation {
    Binder(ParamKind),
    Source(Provenance),
}

The transparent carrier’s payload: a binder’s kind, or where a subterm came from. One piece of information about how a subterm was written. The elaborator and the interface printer read it; every kernel judgment erases it first.

Variants

Binder(ParamKind)

How the argument of the wrapped fun or Π is supplied — Lean’s BinderInfo.

Source(Provenance)

Where the wrapped subterm came from.

Trait Implementations

impl Clone for Annotation

fn clone(&self) -> Annotation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Annotation

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

Formats the value using the given formatter.

impl Display for Annotation

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

Formats the value using the given formatter.

impl PartialEq for Annotation

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

impl StructuralPartialEq for Annotation