Module move_model::simplifier
source · [−]Structs
A rewriter pipeline that is composed of a chain of spec rewriters. Note that this composite rewriter is also a spec rewriter.
Enums
Available simplifications passes to run after tbe model is built
Traits
A generic trait for rewriting the specifications in the GlobalEnv
. A rewriter is expected to
implement at least one rewrite_*
function, depending on which type(s) of specs the rewriter
targets. All the rewrite_*
function should follow the convention on return value: