Trait Theorem 

pub trait Theorem {
    // Required methods
    fn binders(&self) -> Range<usize>;
    fn 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 binders(&self) -> Range<usize>

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

Implementors

impl Theorem for Theorem_