Provides environment extensions around the bv_decide tactic frontends.

opaque Lean.Elab.Tactic.BVDecide.Frontend.sat.solver : Lean.Option String

def Lean.Elab.Tactic.BVDecide.Frontend.elabBVDecideConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig

Equations

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

opaque Lean.Elab.Tactic.BVDecide.Frontend.bvNormalizeExt : Lean.Meta.SimpExtension

opaque Lean.Elab.Tactic.BVDecide.Frontend.builtinBVNormalizeSimprocsRef : IO.Ref Lean.Meta.Simprocs

Builtin bv_normalize simprocs.

opaque Lean.Elab.Tactic.BVDecide.Frontend.bvNormalizeSimprocExt : Lean.Meta.Simp.SimprocExtension

def Lean.Elab.Tactic.BVDecide.Frontend.addBVNormalizeProcBuiltinAttr (declName : Lean.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc) : IO Unit