Struct Sequent 

pub struct Sequent {
    pub linear: Vec<Formula>,
    pub unrestricted: Vec<Formula>,
    pub focus: Option<Formula>,
}

A one-sided sequent ⊢ Γ.

We use a zone-based representation for focused proof search:

• Linear zone: formulas that must be used exactly once
• Unrestricted zone: formulas under ? that can be reused

Fields

linear: Vec<Formula>

Linear hypotheses (multiset, represented as Vec)

unrestricted: Vec<Formula>

Unrestricted hypotheses (under ?)

focus: Option<Formula>

Currently focused formula (if any)

Implementations

impl Sequent

pub fn new(formulas: Vec<Formula>) -> Sequent

Create a new sequent from a list of formulas.

pub fn is_empty(&self) -> bool

Check if sequent is empty (proven).

pub fn focus_on(&self, idx: usize) -> Option<Sequent>

Focus on a formula at the given index.

pub fn unfocus(&self) -> Sequent

Unfocus, returning formula to linear zone.

pub fn pretty(&self) -> String

Pretty print the sequent.

Trait Implementations

impl Clone for Sequent

fn clone(&self) -> Sequent

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Sequent

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

Formats the value using the given formatter.

impl Eq for Sequent

impl Hash for Sequent

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Sequent

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Sequent