Provides environment extensions around the bv_decide tactic frontends.

opaque Lean.Meta.Tactic.BVDecide.sat.solver : Lean.Option String

def Lean.Meta.Tactic.BVDecide.elabBVDecideConfig (cfg : Syntax) (init : Elab.Tactic.BVDecide.BVDecideConfig := { }) (logExceptions : Bool := true) : Elab.Tactic.TacticM Elab.Tactic.BVDecide.BVDecideConfig

def Lean.Meta.Tactic.BVDecide.isPotentialTypeAnalysisType (declName : Name) : CoreM Bool

def Lean.Meta.Tactic.BVDecide.elabBVDecideTypes (stx : Option (TSyntax `Lean.Parser.Tactic.bvTypes)) : CoreM (Option (Array Name))

Elaborate the optional types [T₁, ..., Tₙ] clause of the bv_decide family of tactics. Returns none if the clause is absent, in which case the structure and enum analysis runs unrestricted.

opaque Lean.Meta.Tactic.BVDecide.bvNormalizeExt : Sym.Simp.SymSimpExtension

def Lean.Meta.Tactic.BVDecide.symIntToBitVecName : Name

def Lean.Meta.Tactic.BVDecide.metaIntToBitVecName : Name

opaque Lean.Meta.Tactic.BVDecide.symIntToBitVecExt : Sym.Simp.SymSimpExtension

opaque Lean.Meta.Tactic.BVDecide.metaIntToBitVecExt : SimpExtension