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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvNormalize (g : MVarId) (cfg : BVDecideConfig) :
MetaM (Option MVarId)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.evalBVNormalize :
Tactic
Equations

- One or more equations did not get rendered due to their size.

Instances For