Enum fungi_lang::decide::DecError
source · pub enum DecError {
TypeError(TypeError),
InSubDec,
LamNotArrow,
AppNotArrow,
PairNotProd,
SubsetSearchFailureMisc(String),
SubsetSearchFailureTm(NmSetTm, NmSet),
SubsetSearchFailure(IdxTm, IdxTm),
UnknownCongruence(IdxTm, IdxTm),
}
Expand description
Decision-related error
Variants
TypeError(TypeError)
Type/sort/kind error during the decision procedure
InSubDec
LamNotArrow
AppNotArrow
PairNotProd
SubsetSearchFailureMisc(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 Eq for DecError
impl StructuralEq for DecError
impl StructuralPartialEq for DecError
Auto Trait Implementations
impl !RefUnwindSafe for DecError
impl !Send for DecError
impl !Sync for DecError
impl Unpin for DecError
impl !UnwindSafe for DecError
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more