Type Alias ModalObOp

pub type ModalObOp = Path<ModalObType, ModeApp<ModalOp>>;

An object operation in a modal double theory.

Aliased Type

pub enum ModalObOp {
    Id(ModeApp<QualifiedName>),
    Seq(NonEmpty<ModeApp<ModalOp>>),
}

Variants

Id(ModeApp<QualifiedName>)

The identity, or empty, path at a vertex.

Seq(NonEmpty<ModeApp<ModalOp>>)

A nontrivial path, comprising a non-empty vector of consecutive edges.

Implementations

impl ModalObOp

pub fn ob_act(self, ob: ModalOb) -> Result<ModalOb, String>

Acts on an object in a model of a modal theory.

impl ModalObOp

pub fn generator(id: QualifiedName) -> Self

Constructs the object operation for a generator.

pub fn concat(list: List, arity: usize, ob_type: ModalObType) -> Self

Constructs a concatenation operation for a list modality.

pub fn apply(self, m: Modality) -> Self

Applies a modality.

pub fn apply_all(self, iter: impl IntoIterator<Item = Modality> + Clone) -> Self

Applies a sequence of modalities.