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
opaque Lean.Elab.Tactic.BVDecide.Frontend.sat.timeout :
Lean.Option Nat
source
opaque Lean.Elab.Tactic.BVDecide.Frontend.sat.trimProofs :
Lean.Option Bool
source
opaque Lean.Elab.Tactic.BVDecide.Frontend.sat.binaryProofs :
Lean.Option Bool
source
opaque Lean.Elab.Tactic.BVDecide.Frontend.debug.bv.graphviz :
Lean.Option Bool
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 : Lake.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