Function fungi_lang::decide::effect::decide_idxtm_subtraction

source · 
pub fn decide_idxtm_subtraction(
    ctx: &Ctx,
    i: IdxTm,
    j: IdxTm
) -> Result<IdxTm, Error>
Expand description

Tactic to find an index term j2 such that i = j % j2

TODO: “Verify” the results using our decision procedures; return those derivations with the term that we find