Enum KernelError 

pub enum KernelError {
    UnboundVariable(String),
    NotAFunction(String),
    NotAType(String),
    TypeMismatch {
        expected: String,
        found: String,
    },
    NotAnInductive(String),
    InvalidMotive(String),
    WrongNumberOfCases {
        expected: usize,
        found: usize,
    },
    CertificationError(String),
    TerminationViolation {
        fix_name: String,
        reason: String,
    },
    PositivityViolation {
        inductive: String,
        constructor: String,
        reason: String,
    },
    CannotInferHole,
}

Errors that can occur during type checking.

Variants

UnboundVariable(String)

Reference to an undefined variable.

NotAFunction(String)

Attempted to apply a non-function term.

NotAType(String)

Expected a type (something with type Sort), got something else.

TypeMismatch

Type mismatch: expected one type, found another.

Fields

expected: String

found: String

NotAnInductive(String)

Attempted to match on a non-inductive type.

InvalidMotive(String)

Invalid motive in match expression.

WrongNumberOfCases

Wrong number of cases in match expression.

Fields

expected: usize

found: usize

CertificationError(String)

Error during proof certification.

TerminationViolation

Recursive call does not decrease structurally.

This error prevents infinite loops in proofs. A fixpoint must recurse on a structurally smaller argument.

Fields

fix_name: String

reason: String

PositivityViolation

Inductive type appears in negative position in constructor.

This error prevents logical paradoxes (Russell’s paradox, etc). An inductive must appear strictly positively in its constructors.

Fields

inductive: String

constructor: String

reason: String

CannotInferHole

Cannot infer the type of a hole without context.

Holes (implicit arguments) need to be checked against an expected type, not inferred standalone.

Trait Implementations

impl Debug for KernelError

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

Formats the value using the given formatter.

impl Display for KernelError

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

Formats the value using the given formatter.

impl Error for KernelError

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.

impl From<KernelError> for InterfaceError

fn from(e: KernelError) -> Self

Converts to this type from the input type.