Struct LeanException 

pub struct LeanException { /* private fields */ }

A Lean exception thrown through the IO error channel.

Constructed only by the crate; the kind and message fields are private so the bounded-message invariant survives downstream pattern-matching.

Implementations

impl LeanException

pub fn kind(&self) -> LeanExceptionKind

The IO.Error constructor Lean reported.

Use this to classify a Lean-thrown exception when the caller-facing taxonomy in LeanDiagnosticCode is not specific enough — for example, distinguishing FileNotFound from PermissionDenied to drive different recovery paths.

pub fn message(&self) -> &str

What Lean said about the failure, truncated to at most LEAN_ERROR_MESSAGE_LIMIT bytes on a UTF-8 char boundary.

Trait Implementations

impl Clone for LeanException

fn clone(&self) -> LeanException

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanException

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

Formats the value using the given formatter.

impl Display for LeanException

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

Formats the value using the given formatter.