Enum DiagnosticCode 

pub enum DiagnosticCode {
    InvalidProof,
    MalformedExport,
    UnsupportedExportVersion,
    UnsupportedToolchain,
    UnknownRecordKind,
    UnknownField,
    UnresolvedMetavariable,
    MissingDeclaration,
    DuplicateDeclaration,
    MissingModule,
    ImportCycle,
    LeanRejected,
    LeanAcceptanceNotObserved,
    UnsupportedFeature,
    RecheckRefused,
    AuditIncomplete,
    DisallowedAssumption,
    AssumptionDisagreement,
    ResourceLimit,
    Infrastructure,
    InternalInconsistency,
    Usage,
    Unclassified,
}

Why the reader (or the intake around it) refused. Stable across releases: the wire name is DiagnosticCode::as_str, and a renamed wire name is a protocol break.

Variants

InvalidProof

Well-formed input whose mathematics the kernel refutes: an ill-typed body, a type mismatch, a positivity violation.

MalformedExport

The export itself is malformed: bad JSON, a dangling index, a missing mandatory field.

UnsupportedExportVersion

The export declares a format version this reader does not implement.

UnsupportedToolchain

The export or project was produced by a Lean or exporter outside the pinned profile.

UnknownRecordKind

A record, expression or declaration kind the pinned export format does not define.

UnknownField

A field the pinned export format does not define for its record.

UnresolvedMetavariable

A metavariable or free variable: the declaration was never fully elaborated.

MissingDeclaration

A declaration the input names but never declares, or a target that is not there.

DuplicateDeclaration

A declaration declared twice.

MissingModule

A Lean project imports a module that is neither in the project nor in Lean core.

ImportCycle

A Lean project’s modules import each other in a cycle.

LeanRejected

Lean itself rejected the project’s source (syntax or elaboration), at Lean’s location.

LeanAcceptanceNotObserved

The input is a pre-exported artifact: this run did not observe Lean accepting its source.

UnsupportedFeature

Valid Lean that LOGOS does not yet express faithfully; declined, never approximated.

RecheckRefused

The independent re-checker did not confirm what the primary kernel accepted.

AuditIncomplete

The transitive assumption audit could not be completed.

DisallowedAssumption

The declaration depends on an assumption the policy does not allow.

AssumptionDisagreement

Lean’s #print axioms and the LOGOS audit disagree on a declaration’s assumptions.

ResourceLimit

A declared resource budget was exhausted before a decision.

Infrastructure

The environment failed: a file could not be read, a tool is absent, a thread could not be reserved.

InternalInconsistency

LOGOS’s own artifact — the emitted document, the assembled package, its fresh replay — failed its self-verification after every check of the user’s input passed. The fault is ours, never the user’s mathematics.

Usage

The command was invoked wrongly; nothing ran.

Unclassified

Not yet classified. lean_diagnostic_code_lock drives the number of such sites to zero.

Implementations

impl DiagnosticCode

pub const ALL: [DiagnosticCode; 23]

pub fn as_str(self) -> &'static str

pub fn from_wire(wire: &str) -> Option<DiagnosticCode>

The code a wire name names.

pub fn outcome(self) -> Option<Outcome>

The result outcome this code decides. Usage precedes any result; Unclassified carries no category of its own (see Outcome::of_refusal).

Trait Implementations

impl Clone for DiagnosticCode

fn clone(&self) -> DiagnosticCode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DiagnosticCode

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

Formats the value using the given formatter.

impl Display for DiagnosticCode

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

Formats the value using the given formatter.

impl Hash for DiagnosticCode

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

where __H: Hasher,

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 Ord for DiagnosticCode

fn cmp(&self, other: &DiagnosticCode) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for DiagnosticCode

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

fn partial_cmp(&self, other: &DiagnosticCode) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for DiagnosticCode

impl Eq for DiagnosticCode

impl StructuralPartialEq for DiagnosticCode