Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Attr

Provides environment extensions around the bv_decide tactic frontends.

source
opaque Lean.Elab.Tactic.BVDecide.Frontend.sat.solver :
Lean.Option String
source
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.
Instances For
    source
    opaque Lean.Elab.Tactic.BVDecide.Frontend.bvNormalizeExt :
    Lean.Meta.SimpExtension
    source
    opaque Lean.Elab.Tactic.BVDecide.Frontend.builtinBVNormalizeSimprocsRef :
    IO.Ref Lean.Meta.Simprocs

    Builtin bv_normalize simprocs.

    source
    opaque Lean.Elab.Tactic.BVDecide.Frontend.bvNormalizeSimprocExt :
    Lean.Meta.Simp.SimprocExtension
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.addBVNormalizeProcBuiltinAttr (declName : Lean.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc) :
    IO Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For