Enum EvidenceStatus 

pub enum EvidenceStatus {
    Checked,
    Rejected,
    Unavailable,
    Unsupported,
}

What the kernel-check capability concluded about a piece of Lean source.

The tag accessor on LeanKernelOutcome::status returns values of this type, as does crate::LeanSession::check_evidence when re-validating a captured crate::LeanEvidence handle.

Variants

Checked

The kernel accepted the declaration. A crate::LeanEvidence handle is available on the LeanKernelOutcome::Checked branch.

Rejected

The declaration was well-formed enough to reach kernel checking, and the kernel (or the elaborator’s type-check pass) refused it.

Unavailable

The capability ran but could not produce evidence — typically a parse failure that aborted before the kernel could see the declaration.

Unsupported

The source did not name a kind of declaration this capability produces evidence for (for example a #check command, a non-theorem definition, or a comment-only fragment).

Trait Implementations

impl Clone for EvidenceStatus

fn clone(&self) -> EvidenceStatus

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EvidenceStatus

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

Formats the value using the given formatter.

impl PartialEq for EvidenceStatus

fn eq(&self, other: &EvidenceStatus) -> 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<'lean> TryFromLean<'lean> for EvidenceStatus

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode a nullary-only Lean EvidenceStatus inductive. Lean’s compiler emits a nullary-only inductive as a scalar-tagged pointer (lean_box(tag)) at the top-level boundary rather than a heap-allocated zero-field constructor, so the decoder reads through lean_unbox on the scalar branch and falls back to ctor_tag only if a future encoding shift starts materialising the inductive on the heap.

Tag order is Checked = 0, Rejected = 1, Unavailable = 2, Unsupported = 3, matching the declaration order in fixtures/lean/LeanRsFixture/Elaboration.lean’s EvidenceStatus inductive.

impl Copy for EvidenceStatus

impl Eq for EvidenceStatus

impl StructuralPartialEq for EvidenceStatus