Enum LeanExceptionKind 

#[non_exhaustive]
pub enum LeanExceptionKind {
    AlreadyExists,
    OtherError,
    ResourceBusy,
    ResourceVanished,
    UnsupportedOperation,
    HardwareFault,
    UnsatisfiedConstraints,
    IllegalOperation,
    ProtocolError,
    TimeExpired,
    Interrupted,
    NoFileOrDirectory,
    InvalidArgument,
    PermissionDenied,
    ResourceExhausted,
    InappropriateType,
    NoSuchThing,
    UnexpectedEof,
    UserError,
    Other,
}

Constructor tag for Lean’s IO.Error.

1:1 with IO.Error at the active Lean toolchain version (4.29.1 — see src/lean/Init/System/IOError.lean), plus an Other catch-all for tag values not in the declaration. The crate-internal decoder maps the raw lean_obj_tag to a variant via a const table; a unit test anchors the userError mapping against the live Lean runtime and will fail if the constructor index drifts.

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.

AlreadyExists

IO.Error.alreadyExists

OtherError

IO.Error.otherError

ResourceBusy

IO.Error.resourceBusy

ResourceVanished

IO.Error.resourceVanished

UnsupportedOperation

IO.Error.unsupportedOperation

HardwareFault

IO.Error.hardwareFault

UnsatisfiedConstraints

IO.Error.unsatisfiedConstraints

IllegalOperation

IO.Error.illegalOperation

ProtocolError

IO.Error.protocolError

TimeExpired

IO.Error.timeExpired

Interrupted

IO.Error.interrupted

NoFileOrDirectory

IO.Error.noFileOrDirectory

InvalidArgument

IO.Error.invalidArgument

PermissionDenied

IO.Error.permissionDenied

ResourceExhausted

IO.Error.resourceExhausted

InappropriateType

IO.Error.inappropriateType

NoSuchThing

IO.Error.noSuchThing

UnexpectedEof

IO.Error.unexpectedEof

UserError

IO.Error.userError

Other

Tag did not match any known IO.Error constructor at the active Lean toolchain version.

Trait Implementations

impl Clone for LeanExceptionKind

fn clone(&self) -> LeanExceptionKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanExceptionKind

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

Formats the value using the given formatter.

impl PartialEq for LeanExceptionKind

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for LeanExceptionKind

impl Eq for LeanExceptionKind

impl StructuralPartialEq for LeanExceptionKind