Enum LeanKernelOutcome 

#[non_exhaustive]
pub enum LeanKernelOutcome<'lean> {
    Checked(LeanEvidence<'lean>),
    Rejected(LeanElabFailure),
    Unavailable(LeanElabFailure),
    Unsupported(LeanElabFailure),
}

Outcome of crate::LeanSession::kernel_check.

Carries either a crate::LeanEvidence handle (on Checked) or a LeanElabFailure (on every other status) so callers can both branch on the typed status tag via Self::status and read the structured diagnostics in the failure cases.

#[non_exhaustive] so the variant set tracks future toolchain classification refinements without breaking exhaustive matches.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

Checked(LeanEvidence<'lean>)

The kernel accepted the declaration.

Rejected(LeanElabFailure)

The declaration reached kernel checking and was refused. The failure carries the diagnostics the elaborator and kernel produced.

Unavailable(LeanElabFailure)

The capability could not produce evidence (typically a parse failure). The failure carries the diagnostics Lean produced before aborting.

Unsupported(LeanElabFailure)

The source did not name a supported kind of declaration. The failure carries any diagnostics Lean produced while classifying.

Implementations

impl LeanKernelOutcome<'_>

pub fn status(&self) -> EvidenceStatus

Project the variant tag without consuming the payload.

Useful when the caller only needs to branch on Checked vs. one of the failure tags before deciding whether to read the contained LeanElabFailure diagnostics.

Trait Implementations

impl<'lean> Debug for LeanKernelOutcome<'lean>

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

Formats the value using the given formatter.

impl<'lean> TryFromLean<'lean> for LeanKernelOutcome<'lean>

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

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.