Module fungi_lang::decide::effect

source ·
Expand description

Decide effect relationships

Enums

Error
Effect-related decision errors
Role
Computation role, either Archivist or Editor.

Functions

decide_effect_ceffect_sequencing
The result effect, if it exists, is ceffect3 such that eff1 then ceffect2 = ceffect3
decide_effect_ceffect_sequencing_db
The result effect, if it exists, is ceffect3 such that eff1 then ceffect2 = ceffect3
decide_effect_empty
Decide whether a given effect is empty
decide_effect_sequencing
The result effect, if it exists, is eff3 such that eff1 then eff2 = eff3
decide_effect_sequencing_db
decide_effect_subtraction
Tactic to find the result effect eff3 such that eff1 = eff2 then eff3
decide_effect_subtraction_db
decide_idxtm_cons
Construct a name set (i (cons) j) from name set pair (i,j) and constructor cons.
decide_idxtm_subtraction
Tactic to find an index term j2 such that i = j % j2
decide_nmset_subtraction
Tactic to find an index term j such that NmSet(ns1) == NmSet(ns2) % j
test_idxtm_empty
test_idxtm_equiv