Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Rewrite

This module contains the implementation of the rewriting pass in the fixpoint pipeline, applying rules from the bv_normalize simp set.

Responsible for applying the Bitwuzla style rewrite rules.

Equations
    Instances For