Trait trivial_kernel::table::Theorem

pub trait Theorem {
    fn get_binders(&self) -> Range<usize>;
    fn get_unify_commands(&self) -> Range<usize>;
}

A handle to a theorem.

Theorems in the table only contain the list of binders, and a command stream for unification. The number of hypotheses can be determined by counting the number of Hyp commands in the unification stream.

Required methods

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

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

Loading content...

Implementors

impl Theorem for Theorem_

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

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

Loading content...