Module error 

Typed kernel verdicts.

A Reject is a claim: the input is not a valid Lean environment. A Decline claims nothing: the checker ran out of a resource or met a construct it does not implement. The two are never confused, because a decline reported as a rejection would be a wrong answer on a valid proof.

Structs

Failure

KernelFailure

A Failure behind one pointer. Every step of checking returns a KResult, almost always Ok; boxed, the failure keeps KResult<T> as small as T plus a pointer, so results travel in registers instead of through memory on every call.

Enums

FailKind

Type Aliases

KResult