Skip to main content

Theorem

trivial_kernel::table

Trait Theorem 

Source 
pub trait Theorem {
    // Required methods
    fn binders(&self) -> Range<usize>;
    fn unify_commands(&self) -> Range<usize>;
}
Expand description

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§

Source

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

Source

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

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§