Enum tptp::ast::FofFormula [−][src]
pub enum FofFormula { True, False, Equal(Box<FofTerm>, Box<FofTerm>), Predicate(Name, Vec<Box<FofTerm>>), Not(Box<FofFormula>), And(Vec<Box<FofFormula>>), Or(Vec<Box<FofFormula>>), Implies(Box<FofFormula>, Box<FofFormula>), Equivalent(Box<FofFormula>, Box<FofFormula>), Forall(Vec<Bound>, Box<FofFormula>), Exists(Vec<Bound>, Box<FofFormula>), }
A FOF formula, simplified where possible.
For example, p <~> q
becomes ~(p <=> q)
.
Variants
True
$true
False
$false
Equal(Box<FofTerm>, Box<FofTerm>)
t1 = t2
Predicate(Name, Vec<Box<FofTerm>>)
p(t1, t2, ...)
Not(Box<FofFormula>)
~p
And(Vec<Box<FofFormula>>)
p1 & p2 & ...
Or(Vec<Box<FofFormula>>)
p1 | p2 | ...
Implies(Box<FofFormula>, Box<FofFormula>)
p => q
Equivalent(Box<FofFormula>, Box<FofFormula>)
p <=> q
Forall(Vec<Bound>, Box<FofFormula>)
![X1, X2, ...]: p
Exists(Vec<Bound>, Box<FofFormula>)
?[X1, X2, ...]: p
Trait Implementations
impl Clone for FofFormula
[src]
impl Clone for FofFormula
fn clone(&self) -> FofFormula
[src]
fn clone(&self) -> FofFormula
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read more
impl Debug for FofFormula
[src]
impl Debug for FofFormula
fn fmt(&self, f: &mut Formatter) -> Result
[src]
fn fmt(&self, f: &mut Formatter) -> Result
Formats the value using the given formatter. Read more
impl PartialOrd for FofFormula
[src]
impl PartialOrd for FofFormula
fn partial_cmp(&self, other: &FofFormula) -> Option<Ordering>
[src]
fn partial_cmp(&self, other: &FofFormula) -> Option<Ordering>
This method returns an ordering between self
and other
values if one exists. Read more
fn lt(&self, other: &FofFormula) -> bool
[src]
fn lt(&self, other: &FofFormula) -> bool
This method tests less than (for self
and other
) and is used by the <
operator. Read more
fn le(&self, other: &FofFormula) -> bool
[src]
fn le(&self, other: &FofFormula) -> bool
This method tests less than or equal to (for self
and other
) and is used by the <=
operator. Read more
fn gt(&self, other: &FofFormula) -> bool
[src]
fn gt(&self, other: &FofFormula) -> bool
This method tests greater than (for self
and other
) and is used by the >
operator. Read more
fn ge(&self, other: &FofFormula) -> bool
[src]
fn ge(&self, other: &FofFormula) -> bool
This method tests greater than or equal to (for self
and other
) and is used by the >=
operator. Read more
impl Ord for FofFormula
[src]
impl Ord for FofFormula
fn cmp(&self, other: &FofFormula) -> Ordering
[src]
fn cmp(&self, other: &FofFormula) -> Ordering
This method returns an Ordering
between self
and other
. Read more
fn max(self, other: Self) -> Self
1.21.0[src]
fn max(self, other: Self) -> Self
Compares and returns the maximum of two values. Read more
fn min(self, other: Self) -> Self
1.21.0[src]
fn min(self, other: Self) -> Self
Compares and returns the minimum of two values. Read more
impl PartialEq for FofFormula
[src]
impl PartialEq for FofFormula
fn eq(&self, other: &FofFormula) -> bool
[src]
fn eq(&self, other: &FofFormula) -> bool
This method tests for self
and other
values to be equal, and is used by ==
. Read more
fn ne(&self, other: &FofFormula) -> bool
[src]
fn ne(&self, other: &FofFormula) -> bool
This method tests for !=
.
impl Eq for FofFormula
[src]
impl Eq for FofFormula
Auto Trait Implementations
impl Send for FofFormula
impl Send for FofFormula
impl Sync for FofFormula
impl Sync for FofFormula