Enum ElaborationError 

pub enum ElaborationError {
    Ambiguous(String),
    Cyclic(String),
    LimitExceeded(String),
    CannotReproduce(String),
    Inconclusive(String),
}

Errors that can occur during post-refutation proof elaboration.

Variants

Ambiguous(String)

Multiple distinct rewrite paths could produce the conclusion without a unique canonical trace.

Cyclic(String)

A cyclic rewrite or dependency loop was detected.

LimitExceeded(String)

Search exceeded bounded step limits.

CannotReproduce(String)

Replay could not reproduce the expected conclusion from the specified parents.

Inconclusive(String)

The proof or rule structure is invalid or unsupported.

Trait Implementations

impl Clone for ElaborationError

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ElaborationError

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

Formats the value using the given formatter.

impl Display for ElaborationError

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

Formats the value using the given formatter.

impl Eq for ElaborationError

impl Error for ElaborationError

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 PartialEq for ElaborationError

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ElaborationError