Enum Connective 

pub enum Connective {
    Atom,
    AtomDual,
    Tensor,
    Par,
    Plus,
    With,
    One,
    Bottom,
    Zero,
    Top,
    OfCourse,
    WhyNot,
}

Variants

Atom

A positive literal.

AtomDual

A literal’s linear negation a⊥.

Tensor

A ⊗ B — multiplicative conjunction (“both, together”).

Par

A ⅋ B — multiplicative disjunction.

Plus

A ⊕ B — additive disjunction (internal choice).

With

A & B — additive conjunction (external choice).

One

1 — unit of ⊗.

Bottom

⊥ — unit of ⅋.

Zero

0 — unit of ⊕.

Top

⊤ — unit of &.

OfCourse

!A — exponential “of course” (reusable: weakening + contraction apply).

WhyNot

?A — exponential “why not” (dual of !).

Implementations

impl Connective

pub fn dual(self) -> Connective

Linear negation (·)⊥ — the involutive De Morgan dual (A⊥⊥ = A).

pub fn is_multiplicative(self) -> bool

Multiplicative connectives/units (⊗ ⅋ 1 ⊥).

pub fn is_additive(self) -> bool

Additive connectives/units (⊕ & 0 ⊤).

pub fn is_exponential(self) -> bool

Exponential connectives (! ?).

pub fn is_reusable(self) -> bool

A resource under ! (“of course”) is reusable — structural weakening and contraction are licensed. Everything else is linear (consume-once).

Trait Implementations

impl Clone for Connective

fn clone(&self) -> Connective

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Connective

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for Connective

fn eq(&self, other: &Connective) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for Connective

impl Eq for Connective

impl StructuralPartialEq for Connective