Enum ProofError 

pub enum ProofError {
    NoProofFound,
    DepthExceeded,
    OccursCheck {
        variable: String,
        term: ProofTerm,
    },
    UnificationFailed {
        left: ProofTerm,
        right: ProofTerm,
    },
    ExprUnificationFailed {
        left: ProofExpr,
        right: ProofExpr,
    },
    SymbolMismatch {
        left: String,
        right: String,
    },
    ArityMismatch {
        expected: usize,
        found: usize,
    },
    PatternNotDistinct(String),
    NotAPattern(ProofExpr),
    ScopeViolation {
        var: String,
        allowed: Vec<String>,
    },
}

Errors that can occur during proof search.

Variants

NoProofFound

No proof was found for the given goal.

DepthExceeded

The proof search exceeded the maximum depth limit.

OccursCheck

Unification failed due to occurs check. This prevents infinite types like x = f(x).

Fields

variable: String

term: ProofTerm

UnificationFailed

Unification failed because terms could not be unified.

Fields

left: ProofTerm

right: ProofTerm

ExprUnificationFailed

Expression-level unification failed.

Fields

left: ProofExpr

right: ProofExpr

SymbolMismatch

Symbol mismatch during unification.

Fields

left: String

right: String

ArityMismatch

Arity mismatch during unification.

Fields

expected: usize

found: usize

PatternNotDistinct(String)

The pattern has non-distinct arguments (e.g., ?F(x, x)) Miller patterns require distinct bound variables.

NotAPattern(ProofExpr)

Expression is not a valid Miller pattern. Pattern arguments must be Term(BoundVarRef(…)).

ScopeViolation

RHS uses variables not in pattern scope. In ?P(x) = Body, Body must only use variables that appear in the pattern.

Fields

var: String

allowed: Vec<String>

Trait Implementations

impl Clone for ProofError

fn clone(&self) -> ProofError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofError

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

Formats the value using the given formatter.

impl Display for ProofError

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

Formats the value using the given formatter.

impl Error for ProofError

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.