Struct LinSequent 

pub struct LinSequent {
    pub formulas: Vec<LinFormula>,
}

A one-sided sequent: ⊢ Γ (a multiset of linear formulas).

Fields

formulas: Vec<LinFormula>

Formulas in the succedent (all on the right in one-sided calculus).

Implementations

impl LinSequent

pub fn new(formulas: Vec<LinFormula>) -> Self

Create a new sequent from a list of formulas.

pub fn unit() -> Self

Create the unit sequent ⊢ 1.

pub fn is_axiom(&self) -> bool

Check if this is an identity axiom: ⊢ A, A^⊥.

pub fn tensor_components(&self) -> Option<(LinSequent, LinFormula, LinFormula)>

Apply the tensor rule: split into two sub-sequents. Returns the two components if the sequent has the form ⊢ …, A ⊗ B, …

pub fn display(&self) -> String

Display the sequent as ⊢ A, B, …

pub fn total_complexity(&self) -> usize

Total complexity of all formulas in the sequent.

Trait Implementations

impl Clone for LinSequent

fn clone(&self) -> LinSequent

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LinSequent

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

Formats the value using the given formatter.