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
• restrictedTypes : Option (Array Name)

  The types that the structure and enum analysis is restricted to, as provided by the types clause. If this is none the analysis discovers the relevant types on its own.

def Lean.Meta.Tactic.BVDecide.TacticContext.new (lratPath : System.FilePath) (config : Elab.Tactic.BVDecide.BVDecideConfig) (restrictedTypes : Option (Array Name) := none) : Elab.TermElabM TacticContext