Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVCheck

This modules provides the implementation of bv_check.

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.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Prepare an Expr that proves bvExpr.unsat using ofReduceBool.

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

        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.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For