pub enum TheoryDef {
Discrete(Rc<DiscreteDblTheory>),
DiscreteTab(Rc<DiscreteTabTheory>),
ModalUnital(Rc<ModalDblTheory<Unital>>),
ModalNonUnital(Rc<ModalDblTheory<NonUnital>>),
}Expand description
Definition of a double theory supported by DoubleTT.
Variants§
Discrete(Rc<DiscreteDblTheory>)
A discrete double theory.
DiscreteTab(Rc<DiscreteTabTheory>)
A discrete tabulator theory.
ModalUnital(Rc<ModalDblTheory<Unital>>)
A unital modal double theory.
ModalNonUnital(Rc<ModalDblTheory<NonUnital>>)
A non-unital modal double theory.
Implementations§
Source§impl TheoryDef
impl TheoryDef
Sourcepub fn discrete(theory: DiscreteDblTheory) -> Self
pub fn discrete(theory: DiscreteDblTheory) -> Self
Smart constructor for TheoryDef::Discrete case.
Sourcepub fn discrete_tab(theory: DiscreteTabTheory) -> Self
pub fn discrete_tab(theory: DiscreteTabTheory) -> Self
Smart constructor for TheoryDef::DiscreteTab case.
Sourcepub fn modal_unital(theory: ModalDblTheory<Unital>) -> Self
pub fn modal_unital(theory: ModalDblTheory<Unital>) -> Self
Smart constructor for TheoryDef::ModalUnital case.
Sourcepub fn modal_non_unital(theory: ModalDblTheory<NonUnital>) -> Self
pub fn modal_non_unital(theory: ModalDblTheory<NonUnital>) -> Self
Smart constructor for TheoryDef::ModalNonUnital case.
Sourcepub fn basic_ob_type(&self, name: QualifiedName) -> Option<ObType>
pub fn basic_ob_type(&self, name: QualifiedName) -> Option<ObType>
Gets the basic object type with given name, if it exists.
Sourcepub fn basic_mor_type(&self, name: QualifiedName) -> Option<MorType>
pub fn basic_mor_type(&self, name: QualifiedName) -> Option<MorType>
Gets the basic morphism type with given name, if it exists.
Sourcepub fn basic_ob_op(&self, name: QualifiedName) -> Option<ObOp>
pub fn basic_ob_op(&self, name: QualifiedName) -> Option<ObOp>
Gets the basic object operation with given name, if it exists.
Sourcepub fn hom_type(&self, ob_type: ObType) -> Option<MorType>
pub fn hom_type(&self, ob_type: ObType) -> Option<MorType>
Gets the hom (identity) type for an object type, if it exists.
Sourcepub fn compose_types2(&self, mt1: MorType, mt2: MorType) -> Option<MorType>
pub fn compose_types2(&self, mt1: MorType, mt2: MorType) -> Option<MorType>
Composes a pair of morphism types, if they have a composite.
Trait Implementations§
Source§impl From<Rc<DiscreteDblTheory>> for TheoryDef
impl From<Rc<DiscreteDblTheory>> for TheoryDef
Source§fn from(value: Rc<DiscreteDblTheory>) -> Self
fn from(value: Rc<DiscreteDblTheory>) -> Self
Converts to this type from the input type.
Source§impl From<Rc<DiscreteTabTheory>> for TheoryDef
impl From<Rc<DiscreteTabTheory>> for TheoryDef
Source§fn from(value: Rc<DiscreteTabTheory>) -> Self
fn from(value: Rc<DiscreteTabTheory>) -> Self
Converts to this type from the input type.
Auto Trait Implementations§
impl Freeze for TheoryDef
impl !RefUnwindSafe for TheoryDef
impl !Send for TheoryDef
impl !Sync for TheoryDef
impl Unpin for TheoryDef
impl !UnwindSafe for TheoryDef
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> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
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<T> Pointable for T
impl<T> Pointable for T
§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.