This modules provides the implementation of bv_check.

def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.getSrcDir : TermElabM System.FilePath

Get the directory that contains the Lean file which is currently being elaborated.

def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM TacticContext

def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr

Prepare an Expr that proves bvExpr.unsat using ofReduceBool.

def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"

def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.evalBvCheck : Tactic