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: