This module contains the logic around writing proofs of UNSAT, using LRAT proofs, as meta code.

structure Lean.Meta.Tactic.BVDecide.TacticContext : Type

The context for the bv_decide tactic.

• exprDef : Name
• certDef : Name
• reflectionDef : Name
• solver : System.FilePath
• lratPath : System.FilePath
• config : Elab.Tactic.BVDecide.BVDecideConfig

def Lean.Meta.Tactic.BVDecide.TacticContext.new (lratPath : System.FilePath) (config : Elab.Tactic.BVDecide.BVDecideConfig) : Elab.TermElabM TacticContext

Equations

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