pub enum InstanceJudgment {
Generator(InstanceGenDecl),
Import(InstanceImport),
Equation(InstanceEqnDecl),
}Expand description
A judgment defining part of an instance of a model of a double theory.
Instance notebooks target presentations of instances via fibered generators plus equations between morphism actions on them, in contrast to diagram judgments, which present instances less efficiently via a model morphism.
Variants§
Generator(InstanceGenDecl)
Declares a generator of the instance.
Import(InstanceImport)
Imports another instance of the codomain model.
Equation(InstanceEqnDecl)
Declares an equation between two instance terms.
Trait Implementations§
Source§impl Debug for InstanceJudgment
impl Debug for InstanceJudgment
Source§impl<'de> Deserialize<'de> for InstanceJudgment
impl<'de> Deserialize<'de> for InstanceJudgment
Source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
Source§impl From<InstanceJudgment> for JsValuewhere
InstanceJudgment: Serialize,
impl From<InstanceJudgment> for JsValuewhere
InstanceJudgment: Serialize,
Source§fn from(value: InstanceJudgment) -> Self
fn from(value: InstanceJudgment) -> Self
Converts to this type from the input type.
Source§impl FromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
impl FromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
Source§impl IntoWasmAbi for &InstanceJudgmentwhere
InstanceJudgment: Serialize,
impl IntoWasmAbi for &InstanceJudgmentwhere
InstanceJudgment: Serialize,
Source§impl IntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
impl IntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
Source§impl OptionFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
impl OptionFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
Source§impl OptionIntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
impl OptionIntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
Source§impl PartialEq for InstanceJudgment
impl PartialEq for InstanceJudgment
Source§impl RefFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
impl RefFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
Source§type Abi = <JsType as RefFromWasmAbi>::Abi
type Abi = <JsType as RefFromWasmAbi>::Abi
The Wasm ABI type references to
Self are recovered from.Source§type Anchor = SelfOwner<InstanceJudgment>
type Anchor = SelfOwner<InstanceJudgment>
The type that holds the reference to
Self for the duration of the
invocation of the function that has an &Self parameter. This is
required to ensure that the lifetimes don’t persist beyond one function
call, and so that they remain anonymous.Source§impl Serialize for InstanceJudgment
impl Serialize for InstanceJudgment
Source§impl Tsify for InstanceJudgment
impl Tsify for InstanceJudgment
const DECL: &'static str = "/**\n * A judgment defining part of an instance of a model of a double theory.\n *\n * Instance notebooks target presentations of instances\n * via fibered generators plus equations between morphism actions on them, in\n * contrast to [diagram judgments](super::diagram_judgment::DiagramJudgment),\n * which present instances less efficiently via a model morphism.\n */\nexport type InstanceJudgment = ({ tag: \"generator\" } & InstanceGenDecl) | ({ tag: \"import\" } & InstanceImport) | ({ tag: \"equation\" } & InstanceEqnDecl);"
const SERIALIZATION_CONFIG: SerializationConfig
type JsType = JsType
fn into_js(&self) -> Result<Self::JsType, Error>where
Self: Serialize,
fn from_js<T>(js: T) -> Result<Self, Error>
Source§impl VectorFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
impl VectorFromWasmAbi for InstanceJudgmentwhere
Self: DeserializeOwned,
type Abi = <JsType as VectorFromWasmAbi>::Abi
unsafe fn vector_from_abi(js: Self::Abi) -> Box<[Self]>
Source§impl VectorIntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
impl VectorIntoWasmAbi for InstanceJudgmentwhere
InstanceJudgment: Serialize,
type Abi = <JsType as VectorIntoWasmAbi>::Abi
fn vector_into_abi(vector: Box<[Self]>) -> Self::Abi
Source§impl WasmDescribeVector for InstanceJudgment
impl WasmDescribeVector for InstanceJudgment
impl Eq for InstanceJudgment
impl StructuralPartialEq for InstanceJudgment
Auto Trait Implementations§
impl Freeze for InstanceJudgment
impl RefUnwindSafe for InstanceJudgment
impl Send for InstanceJudgment
impl Sync for InstanceJudgment
impl Unpin for InstanceJudgment
impl UnwindSafe for InstanceJudgment
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
§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 moreSource§impl<T> ReturnWasmAbi for Twhere
T: IntoWasmAbi,
impl<T> ReturnWasmAbi for Twhere
T: IntoWasmAbi,
Source§type Abi = <T as IntoWasmAbi>::Abi
type Abi = <T as IntoWasmAbi>::Abi
Same as
IntoWasmAbi::AbiSource§fn return_abi(self) -> <T as ReturnWasmAbi>::Abi
fn return_abi(self) -> <T as ReturnWasmAbi>::Abi
Same as
IntoWasmAbi::into_abi, except that it may throw and never
return in the case of Err.