Documentation

Lean.Meta.Tactic.BVDecide.Attr

Provides environment extensions around the bv_decide tactic frontends.

source
opaque Lean.Meta.Tactic.BVDecide.sat.solver :
Lean.Option String
source
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.
Instances For
    source
    opaque Lean.Meta.Tactic.BVDecide.bvNormalizeExt :
    SimpExtension
    source
    def Lean.Meta.Tactic.BVDecide.symIntToBitVecName :
    Name
    Equations
    Instances For
      source
      def Lean.Meta.Tactic.BVDecide.metaIntToBitVecName :
      Name
      Equations
      Instances For
        source
        opaque Lean.Meta.Tactic.BVDecide.symIntToBitVecExt :
        Sym.Simp.SymSimpExtension
        source
        opaque Lean.Meta.Tactic.BVDecide.metaIntToBitVecExt :
        SimpExtension
        source
        opaque Lean.Meta.Tactic.BVDecide.builtinBVNormalizeSimprocsRef :
        IO.Ref Simprocs

        Builtin bv_normalize simprocs.

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