pub enum Error {
NoSuchObjectType(QualifiedName),
NoSuchVariable(VarName),
TabulatorUnsupported,
ModalUnsupported,
NonDiscreteUnsupported,
ExpectedObject,
MismatchedDomTypes {
expected: ObjectType,
synthesized: ObjectType,
},
MismatchedCodTypes {
expected: ObjectType,
synthesized: ObjectType,
},
}Expand description
An elaboration error
Variants§
NoSuchObjectType(QualifiedName)
The theory does not contain this object type
NoSuchVariable(VarName)
There is no such variable in scope
TabulatorUnsupported
Tried to elaborate a notebook that uses tabulator features
ModalUnsupported
Tried to elaborate a notebook that uses modal features
NonDiscreteUnsupported
Tried to elaborate a notebook that uses a non-discrete double theory
ExpectedObject
Expected a variable to refer to an object
MismatchedDomTypes
The variable in the domain slot of an arrow doesn’t have the right object type
Fields
§
expected: ObjectTypeThe expected object type
§
synthesized: ObjectTypeThe object type of the variable given
MismatchedCodTypes
The variable in the codomain slot of an arrow doesn’t have the right object type
Fields
§
expected: ObjectTypeThe expected object type
§
synthesized: ObjectTypeThe object type of the variable given
Trait Implementations§
Auto Trait Implementations§
impl Freeze for Error
impl RefUnwindSafe for Error
impl Send for Error
impl Sync for Error
impl Unpin for Error
impl UnwindSafe for Error
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
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more§impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
§fn to_subset(&self) -> Option<SS>
fn to_subset(&self) -> Option<SS>
The inverse inclusion map: attempts to construct
self from the equivalent element of its
superset. Read more§fn is_in_subset(&self) -> bool
fn is_in_subset(&self) -> bool
Checks if
self is actually part of its subset T (and can be converted to it).§fn to_subset_unchecked(&self) -> SS
fn to_subset_unchecked(&self) -> SS
Use with care! Same as
self.to_subset but without any property checks. Always succeeds.§fn from_subset(element: &SS) -> SP
fn from_subset(element: &SS) -> SP
The inclusion map: converts
self to the equivalent element of its superset.