Enum ConstructiveProp 

pub enum ConstructiveProp {
    True,
    False,
    And(Box<ConstructiveProp>, Box<ConstructiveProp>),
    Or(Box<ConstructiveProp>, Box<ConstructiveProp>),
    Not(Box<ConstructiveProp>),
    Implies(Box<ConstructiveProp>, Box<ConstructiveProp>),
    Exists(String, Box<ConstructiveProp>),
    Forall(String, Box<ConstructiveProp>),
    Atom(String, Vec<String>),
    Eq(String, String),
}

A constructive proposition in intuitionistic logic.

Variants

True

Logical truth (⊤).

False

Logical falsehood (⊥).

And(Box<ConstructiveProp>, Box<ConstructiveProp>)

Conjunction (P ∧ Q).

Or(Box<ConstructiveProp>, Box<ConstructiveProp>)

Disjunction (P ∨ Q).

Not(Box<ConstructiveProp>)

Negation (¬P), defined as P → ⊥.

Implies(Box<ConstructiveProp>, Box<ConstructiveProp>)

Implication (P → Q).

Exists(String, Box<ConstructiveProp>)

Existential quantification (∃x. P(x)).

Forall(String, Box<ConstructiveProp>)

Universal quantification (∀x. P(x)).

Atom(String, Vec<String>)

Atomic proposition with arguments.

Eq(String, String)

Propositional equality of two terms.

Trait Implementations

impl Clone for ConstructiveProp

fn clone(&self) -> ConstructiveProp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ConstructiveProp

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

Formats the value using the given formatter.

impl Eq for ConstructiveProp

impl PartialEq for ConstructiveProp

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ConstructiveProp