Trait trivial_kernel::stream::proof::Proof[−][src]

pub trait Proof<T> where
    T: Table, {
    fn end(&mut self) -> KResult;

    fn reference(&mut self, idx: u32) -> KResult;

    fn dummy(&mut self, table: &T, sort: u32, current_sort: u32) -> KResult;

    fn term(
        &mut self, 
        table: &T, 
        idx: u32, 
        current_term: u32, 
        save: bool, 
        def: bool
    ) -> KResult;

    fn theorem(&mut self, table: &T, idx: u32, save: bool) -> KResult;

    fn theorem_start(
        &mut self, 
        table: &T, 
        idx: u32, 
        current_theorem: u32, 
        save: bool
    ) -> KResult<(Stepper, Ptr, bool)>;

    fn theorem_end(&mut self, target: Ptr, save: bool) -> KResult;

    fn hyp(&mut self, table: &T) -> KResult;

    fn conv(&mut self) -> KResult;

    fn refl(&mut self) -> KResult;

    fn symm(&mut self) -> KResult;

    fn cong(&mut self) -> KResult;

    fn unfold_start(&mut self, table: &T) -> KResult<(Stepper, Ptr, Ptr)>;

    fn unfold_end(&mut self, t_ptr: Ptr, e: Ptr) -> KResult;

    fn unfold(&mut self, table: &T) -> KResult;

    fn conv_cut(&mut self) -> KResult;

    fn conv_ref(&mut self, idx: u32) -> KResult;

    fn conv_save(&mut self) -> KResult;

    fn save(&mut self) -> KResult;

    fn execute(
        &mut self, 
        table: &T, 
        state: &State, 
        command: Command<Proof>, 
        is_definition: bool
    ) -> KResult<bool> { ... }

    fn step(
        &mut self, 
        table: &T, 
        state: &State, 
        command: Command<Proof>, 
        is_definition: bool
    ) -> KResult<Option<FinalizeState>> { ... }
}

Required methods

fn end(&mut self) -> KResult[src]

fn reference(&mut self, idx: u32) -> KResult[src]

fn dummy(&mut self, table: &T, sort: u32, current_sort: u32) -> KResult[src]

fn term(
    &mut self,
    table: &T,
    idx: u32,
    current_term: u32,
    save: bool,
    def: bool
) -> KResult[src]

fn theorem(&mut self, table: &T, idx: u32, save: bool) -> KResult[src]

fn theorem_start(
    &mut self,
    table: &T,
    idx: u32,
    current_theorem: u32,
    save: bool
) -> KResult<(Stepper, Ptr, bool)>[src]

fn theorem_end(&mut self, target: Ptr, save: bool) -> KResult[src]

fn hyp(&mut self, table: &T) -> KResult[src]

fn conv(&mut self) -> KResult[src]

fn refl(&mut self) -> KResult[src]

fn symm(&mut self) -> KResult[src]

fn cong(&mut self) -> KResult[src]

fn unfold_start(&mut self, table: &T) -> KResult<(Stepper, Ptr, Ptr)>[src]

fn unfold_end(&mut self, t_ptr: Ptr, e: Ptr) -> KResult[src]

fn unfold(&mut self, table: &T) -> KResult[src]

fn conv_cut(&mut self) -> KResult[src]

fn conv_ref(&mut self, idx: u32) -> KResult[src]

fn conv_save(&mut self) -> KResult[src]

fn save(&mut self) -> KResult[src]

Loading content...

Provided methods

fn execute(
    &mut self,
    table: &T,
    state: &State,
    command: Command<Proof>,
    is_definition: bool
) -> KResult<bool>[src]

fn step(
    &mut self,
    table: &T,
    state: &State,
    command: Command<Proof>,
    is_definition: bool
) -> KResult<Option<FinalizeState>>[src]

Loading content...

Implementors

impl<T, S: Store> Proof<T> for Context<S> where
    T: Table<Var = S::Var>, [src]

Loading content...