Trait Proof

Source

pub trait Proof<T>where
    T: Table,{
Show 21 methods    // Required methods
    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;

    // Provided methods
    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>> { ... }
}