Struct Sequent 

pub struct Sequent {
    pub free_vars: Vec<V>,
    pub body_literals: Vec<Literal>,
    pub head_literals: Vec<Vec<Literal>>,
    /* private fields */
}

Is represented by a list of Literals in the body and a list of list of Literals in the head.

Fields

free_vars: Vec<V>

Is the list of free variables in the sequent and is used for memoization.

body_literals: Vec<Literal>

Represents the body of the sequent as a list of Literals. The literals in body_literals are assumed to be conjoined.

Note: See here for more information about the structure of geometric sequents.

head_literals: Vec<Vec<Literal>>

Represents the head of the sequent as a list of list of Literals. The literals in each sublist of head_literals are assumed to be conjoined where the sublists are disjointed with each other.

Note: See here for more information about the structure of geometric sequents.

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 Display for Sequent

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

Formats the value using the given formatter.

impl From<&Formula> for Sequent

fn from(formula: &Formula) -> Self

Converts to this type from the input type.

impl SequentTrait for Sequent

fn body(&self) -> Formula

Returns the body (premise) of the sequent as a formula.

fn head(&self) -> Formula

Returns the head (consequence) of the sequent as a formula.