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.

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.rewriteRulesPass :
Pass

Responsible for applying the Bitwuzla style rewrite rules.

Equations
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.rewriteRulesPass.getHyps (goal : MVarId) :
      PreProcessM (Array FVarId)
      Equations
        Instances For