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

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

    fn is_definition(&self) -> bool;

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

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

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

A handle to a term.

Associated Types

type Type: Var[src]

Loading content...

Required methods

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

Returns the index of the sort this term has.

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

Returns if this term is a definition.

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

fn get_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 get_return_type(&self) -> &Self::Type[src]

Returns the type of the expression.

fn get_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...