Enum fungi_lang::decide::DecError

pub enum DecError {
    TypeError(TypeError),
    InSubDec,
    LamNotArrow,
    AppNotArrow,
    PairNotProd,
    SubsetSearchFailureMisc(String),
    SubsetSearchFailureTm(NmSetTm, NmSet),
    SubsetSearchFailure(IdxTm, IdxTm),
    UnknownCongruence(IdxTm, IdxTm),
}

Decision-related error

Variants

TypeError(TypeError)

Type/sort/kind error during the decision procedure

InSubDecLamNotArrowAppNotArrowPairNotProdSubsetSearchFailureMisc(String)

search-based decision procedure fails to find proof of a subset relation

SubsetSearchFailureTm(NmSetTm, NmSet)

search-based decision procedure fails to find proof of a membership/subset relation for a name set term

SubsetSearchFailure(IdxTm, IdxTm)

search-based decision procedure fails to find proof of a membership/subset relation for a name set term

UnknownCongruence(IdxTm, IdxTm)

Unknown case of congruence (could be a mismatch)

Trait Implementations

impl Display for DecError

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

Formats the value using the given formatter.

impl Clone for DecError

fn clone(&self) -> DecError

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for DecError

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

Formats the value using the given formatter.

impl Eq for DecError

impl PartialEq for DecError

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl Hash for DecError

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

Feeds a slice of this type into the given [Hasher].