Enum LeanMetaResponse 

#[non_exhaustive]
pub enum LeanMetaResponse<Resp> {
    Ok(Resp),
    Failed(LeanElabFailure),
    TimeoutOrHeartbeat(LeanElabFailure),
    Unsupported(LeanElabFailure),
}

Outcome of a bounded MetaM service call.

Carries either a typed Resp payload (on Ok) 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.

Ok(Resp)

The MetaM action returned a typed payload.

Failed(LeanElabFailure)

The MetaM action raised a non-resource-exhaustion exception. The failure carries one error-severity diagnostic.

TimeoutOrHeartbeat(LeanElabFailure)

The heartbeat ceiling tripped before the action finished. The failure carries the heartbeat-exhaustion message Lean produced.

Unsupported(LeanElabFailure)

The capability did not provide this service. Either the Lean shim returned unsupported or the dispatcher synthesised this branch when the service’s symbol was absent at capability load.

Implementations

impl<Resp> LeanMetaResponse<Resp>

pub fn status(&self) -> MetaCallStatus

Project the variant tag without inspecting the payload.

pub const fn code(&self) -> Option<LeanDiagnosticCode>

Project to the stable LeanDiagnosticCode taxonomy.

Ok returns None — the response carries a typed payload, not a diagnostic. The three failure variants map to LeanDiagnosticCode::Elaboration (the failure carries a LeanElabFailure in every case except Unsupported, which projects to LeanDiagnosticCode::Unsupported).

Trait Implementations

impl<Resp: Debug> Debug for LeanMetaResponse<Resp>

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

Formats the value using the given formatter.

impl<'lean, Resp> TryFromLean<'lean> for LeanMetaResponse<Resp>

where Resp: TryFromLean<'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.