Struct TwoSidedSequent 

pub struct TwoSidedSequent {
    pub antecedent: Vec<Formula>,
    pub succedent: Vec<Formula>,
}

A two-sided sequent Γ ⊢ Δ (for user-facing API).

Fields

antecedent: Vec<Formula>

Left side of the turnstile (antecedent)

succedent: Vec<Formula>

Right side of the turnstile (succedent)

Implementations

impl TwoSidedSequent

pub fn new(antecedent: Vec<Formula>, succedent: Vec<Formula>) -> TwoSidedSequent

Create a new two-sided sequent.

pub fn to_one_sided(&self) -> Sequent

Convert to one-sided: Γ ⊢ Δ becomes ⊢ Γ⊥, Δ

pub fn pretty(&self) -> String

Pretty print the sequent.

Trait Implementations

impl Clone for TwoSidedSequent

fn clone(&self) -> TwoSidedSequent

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TwoSidedSequent

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

Formats the value using the given formatter.

impl Eq for TwoSidedSequent

impl PartialEq for TwoSidedSequent

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for TwoSidedSequent