Enum LeanExceptionKind 

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

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 Copy for LeanExceptionKind

impl Debug for LeanExceptionKind

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

Formats the value using the given formatter.

impl Eq for LeanExceptionKind

impl PartialEq for LeanExceptionKind

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LeanExceptionKind