Enum LeanError 

#[non_exhaustive]
pub enum LeanError {
    LeanException(LeanException),
    Host(HostFailure),
    Cancelled(LeanCancelled),
}

Errors reported across the safe lean-rs boundary.

#[non_exhaustive] so future toolchain or platform refinements can add new diagnostic tags inside HostStage / LeanExceptionKind without breaking pattern-matching code that already handles the top-level variants.

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.

LeanException(LeanException)

Lean threw through its IO error channel; see LeanException.

Host(HostFailure)

The host stack failed at a particular stage; see HostFailure.

Cancelled(LeanCancelled)

A cooperative cancellation token was observed before dispatch.

Implementations

impl LeanError

pub fn code(&self) -> LeanDiagnosticCode

Project to the stable LeanDiagnosticCode taxonomy.

LeanException always maps to LeanDiagnosticCode::LeanException; Host returns the code recorded by the construction site.

Trait Implementations

impl Clone for LeanError

fn clone(&self) -> LeanError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanError

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

Formats the value using the given formatter.

impl Display for LeanError

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

Formats the value using the given formatter.

impl Error for LeanError

fn source(&self) -> Option<&(dyn Error + 'static)>

Returns the lower-level source of this error, if any.

fn description(&self) -> &str

👎Deprecated since 1.42.0:

use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎Deprecated since 1.33.0:

replaced by Error::source, which can support downcasting

fn provide<'a>(&'a self, request: &mut Request<'a>)

🔬This is a nightly-only experimental API. (error_generic_member_access)

Provides type-based access to context intended for error reports.