Enum TransportedTheoremBoundaryValidationError 

pub enum TransportedTheoremBoundaryValidationError {
    RustAdmissionKeyNotRuntimeCritical(String),
    LeanOnlyRuntimeCriticalMissingAssumptionBoundary(String),
    RuntimeProfileMissingRustAdmissionKey(String),
    RuntimeProfileDisablesRustAdmissionKey(String),
    RuntimeProfileEnablesUnknownRustAdmissionKey(String),
}

Reasons the transported-theorem ledger and runtime profile can be inconsistent.

Variants

RustAdmissionKeyNotRuntimeCritical(String)

Rust runtime admission consumes a theorem family that is not classified as runtime-critical in the boundary ledger.

LeanOnlyRuntimeCriticalMissingAssumptionBoundary(String)

A runtime-critical theorem consumed only by Lean lost its explicit assumption boundary marker.

RuntimeProfileMissingRustAdmissionKey(String)

A Rust-runtime-consumed theorem family is missing from the runtime execution profile eligibility set.

RuntimeProfileDisablesRustAdmissionKey(String)

A Rust-runtime-consumed theorem family is present in the runtime profile but disabled.

RuntimeProfileEnablesUnknownRustAdmissionKey(String)

The runtime profile enables a theorem family that is not classified as a Rust-runtime-consumed theorem boundary entry.

Trait Implementations

impl Clone for TransportedTheoremBoundaryValidationError

fn clone(&self) -> TransportedTheoremBoundaryValidationError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TransportedTheoremBoundaryValidationError

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

Formats the value using the given formatter.

impl PartialEq for TransportedTheoremBoundaryValidationError

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

impl StructuralPartialEq for TransportedTheoremBoundaryValidationError