Trait trivial_kernel::table::Term[−][src]

pub trait Term {
    type Type: Var;
    fn sort_idx(&self) -> u8;

    fn is_definition(&self) -> bool;

    fn binders(&self) -> Range<usize>;

    fn return_type(&self) -> &Self::Type;

    fn command_stream(&self) -> Range<usize>;
}

A handle to a term.

Associated Types

type Type: Var[src]

Loading content...

Required methods

fn sort_idx(&self) -> u8[src]

Returns the index of the sort this term has.

fn is_definition(&self) -> bool[src]

Returns true if this term is a definition, and false otherwise.

Definitions are always conservative and can be unfolded in a proof.

fn binders(&self) -> Range<usize>[src]

Returns the range of the binders (arguments) of the term.

The range can be queried in the Table to get the binders themselves.

fn return_type(&self) -> &Self::Type[src]

Returns the type of the expression.

fn command_stream(&self) -> Range<usize>[src]

Returns the unification command stream if this term is a definition.

Loading content...

Implementors

impl Term for Term_[src]

type Type = Var_

Loading content...