Type Alias cop::tptp::STerm

pub type STerm = Term<String, String>;

String term.

Aliased Type

enum STerm {
    C(String, Args<Term<String, String>>),
    V(String),
}

Variants

C(String, Args<Term<String, String>>)

Constant with arguments applied to it

V(String)

Variable

Implementations

impl<C, V> Term<C, V>

pub fn map_constants<D>(self, f: &mut impl FnMut(C) -> D) -> Term<D, V>

Apply function to the constants of the term.

pub fn map_vars<W>(self, f: &mut impl FnMut(V) -> Term<C, W>) -> Term<C, W>

Apply function to the variables of the term.

pub fn constants(&self) -> Box<dyn Iterator<Item = (&C, usize)> + '_>

Return all constants occurring in the term.

pub fn vars(&self) -> Box<dyn Iterator<Item = &V> + '_>

Return all variables occurring in the term.

impl<C: Clone, V: Clone + Eq + Hash> Term<C, V>

pub fn subst(self, sub: &HashMap<V, Term<C, V>>) -> Self

Apply a substitution to the term.

impl<C: Eq, V> Term<C, V>

pub fn const_unique(&self) -> Vec<(&C, usize)>

Corresponds to leanCoP’s collect_func.

impl<C: Fresh, V> Term<C, V>

pub fn skolem(st: &mut C::State, args: Vec<V>) -> Self

Return a fresh Skolem function and apply a sequence of variables.

Trait Implementations

impl<C: Clone, V: Clone> Clone for Term<C, V>

fn clone(&self) -> Term<C, V>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<C: Debug, V: Debug> Debug for Term<C, V>

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

Formats the value using the given formatter.

impl<C: Display, V: Display> Display for Term<C, V>

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

Formats the value using the given formatter.

impl From<DefinedTerm<'_>> for STerm

fn from(tm: DefinedTerm<'_>) -> Self

Converts to this type from the input type.

impl From<DefinedTerm<'_>> for STerm

fn from(tm: DefinedTerm<'_>) -> Self

Converts to this type from the input type.

impl From<FunctionTerm<'_>> for STerm

fn from(tm: FunctionTerm<'_>) -> Self

Converts to this type from the input type.

impl From<PlainTerm<'_>> for STerm

fn from(tm: PlainTerm<'_>) -> Self

Converts to this type from the input type.

impl From<Term<'_>> for STerm

fn from(tm: Term<'_>) -> Self

Converts to this type from the input type.

impl<C: PartialEq, V: PartialEq> PartialEq<Term<C, V>> for Term<C, V>

fn eq(&self, other: &Term<C, V>) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<C: Eq, V: Eq> Eq for Term<C, V>

impl<C, V> StructuralEq for Term<C, V>

impl<C, V> StructuralPartialEq for Term<C, V>