Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVCheck

This modules provides the implementation of bv_check.

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

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.mkContext (lratPath : System.FilePath) :
Lean.Elab.TermElabM Lean.Elab.Tactic.BVDecide.Frontend.TacticContext
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.lratChecker (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) (bvExpr : Std.Tactic.BVDecide.BVLogicalExpr) :
Lean.MetaM Lean.Expr

Prepare an Expr that proves bvExpr.unsat using ofReduceBool.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.bvCheck (g : Lean.MVarId) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) :
Lean.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"
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.evalBvCheck :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.