Term

trivial_kernel::table

Trait Term 

Source 
pub trait Term {
    type Type: Var;

    // Required methods
    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>;
}
Expand description

A handle to a term.

Required Associated Types§

Source

type Type: Var

Required Methods§

Source

fn sort_idx(&self) -> u8

Returns the index of the sort this term has.

Source

fn is_definition(&self) -> bool

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

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

Source

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

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

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

Source

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

Returns the type of the expression.

Source

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

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

Implementors§