pub enum ElabErrorCode {
Show 15 variants
UnknownName,
TypeMismatch,
UnsolvedMvar,
AmbiguousInstance,
NoInstance,
UnificationFailed,
IllTyped,
TacticFailed,
NonExhaustiveMatch,
SyntaxError,
KernelRejected,
SorryNotAllowed,
RecursionLimit,
MutualCycle,
Other,
}Expand description
Structured error codes for elaboration failures.
Variants§
UnknownName
A name was not found in scope.
TypeMismatch
Type mismatch: expected vs. actual type differ.
UnsolvedMvar
A metavariable could not be solved.
AmbiguousInstance
Multiple typeclass instances match.
NoInstance
No typeclass instance found.
UnificationFailed
Unification failed.
IllTyped
Expression is ill-typed.
TacticFailed
Tactic execution failed.
NonExhaustiveMatch
Pattern matching is not exhaustive.
SyntaxError
Syntax error (propagated from parser).
KernelRejected
The kernel rejected the term.
SorryNotAllowed
Sorry was used but not allowed.
RecursionLimit
Recursion limit exceeded.
MutualCycle
Mutual recursion cycle detected.
Other
Other/unclassified error.
Trait Implementations§
Source§impl Clone for ElabErrorCode
impl Clone for ElabErrorCode
Source§fn clone(&self) -> ElabErrorCode
fn clone(&self) -> ElabErrorCode
Returns a duplicate of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for ElabErrorCode
impl Debug for ElabErrorCode
Source§impl Display for ElabErrorCode
impl Display for ElabErrorCode
Source§impl PartialEq for ElabErrorCode
impl PartialEq for ElabErrorCode
impl Eq for ElabErrorCode
impl StructuralPartialEq for ElabErrorCode
Auto Trait Implementations§
impl Freeze for ElabErrorCode
impl RefUnwindSafe for ElabErrorCode
impl Send for ElabErrorCode
impl Sync for ElabErrorCode
impl Unpin for ElabErrorCode
impl UnsafeUnpin for ElabErrorCode
impl UnwindSafe for ElabErrorCode
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more