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 Copy for EvidenceStatus

impl Debug for EvidenceStatus

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

Formats the value using the given formatter.

impl Eq for EvidenceStatus

impl PartialEq for EvidenceStatus

fn eq(&self, other: &EvidenceStatus) -> bool

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for EvidenceStatus

impl<'lean> TryFromLean<'lean> for EvidenceStatus

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

Decode a nullary-only Lean EvidenceStatus inductive.

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