Enum EmissionFault 

pub enum EmissionFault {
    Reparse {
        message: String,
    },
    CommandCount {
        expected: usize,
        found: usize,
    },
    Missing {
        logos: String,
    },
    Kind {
        logos: String,
        expected: DeclarationKind,
    },
    Levels {
        logos: String,
        expected: Vec<String>,
        found: Vec<String>,
    },
    Type {
        logos: String,
    },
    Body {
        logos: String,
    },
    Constructors {
        logos: String,
    },
    Undeclared {
        logos: String,
    },
    Statement {
        logos: String,
    },
    Unmapped {
        name: String,
    },
    Recheck {
        logos: String,
    },
    Structure {
        logos: String,
    },
}

Why an emitted document does not reparse to the imported declarations. Every variant names the LOGOS declaration it concerns.

Variants

Reparse

The fresh context refused the document.

Fields

message: String

CommandCount

The document holds a different number of declaration commands than it should.

Fields

expected: usize

found: usize

Missing

A declaration the document must declare is absent.

Fields

logos: String

Kind

A declaration was registered as a different kind (a theorem that unfolds, an axiom with a proof, …).

Fields

logos: String

expected: DeclarationKind

Levels

A declaration’s universe parameters differ.

Fields

logos: String

expected: Vec<String>

found: Vec<String>

Type

A declaration’s type differs.

Fields

logos: String

Body

A transparent definition’s body differs.

Fields

logos: String

Constructors

An inductive’s parameter count or constructors differ.

Fields

logos: String

Undeclared

The document declared something its correspondence does not list.

Fields

logos: String

Statement

The target’s reparsed statement differs from the reference translation of the Lean type.

Fields

logos: String

Unmapped

A reference term names a constant the correspondence does not map.

Fields

name: String

Recheck

The independent re-checker did not confirm a reparsed definition at its declared type.

Fields

logos: String

Structure

An inductive gained, lost or changed its structure η (its projections).

Fields

logos: String

Trait Implementations

impl Clone for EmissionFault

fn clone(&self) -> EmissionFault

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EmissionFault

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

Formats the value using the given formatter.

impl Display for EmissionFault

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

Formats the value using the given formatter.

impl PartialEq for EmissionFault

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

impl StructuralPartialEq for EmissionFault