Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize

This module contains the implementation of bv_normalize, the preprocessing tactic for bv_decide. It is in essence a (slightly reduced) version of the Bitwuzla preprocessor together with Lean specific details.

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.passPipeline :
PreProcessM (List Pass)
Equations
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvNormalize (g : MVarId) (cfg : BVDecideConfig) :
      MetaM (Option MVarId)
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvNormalize.go (g : MVarId) :
          PreProcessM (Option MVarId)
          Equations
            Instances For
              source
              def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.evalBVNormalize :
              Tactic
              Equations
                Instances For