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

Equations

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

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

Equations

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

def Lean.Meta.Tactic.BVDecide.elabBVDecideTypes (stx : Option (TSyntax `Lean.Parser.Tactic.bvTypes)) (cfg : Elab.Tactic.BVDecide.BVDecideConfig) : 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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Tactic.BVDecide.elabBVDecideTypes stx cfg = pure none

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

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

Equations

• Lean.Meta.Tactic.BVDecide.symIntToBitVecName = `int_toBitVec_sym

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

Equations

• Lean.Meta.Tactic.BVDecide.metaIntToBitVecName = `int_toBitVec_meta

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

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