Documentation

Lean.Elab.Tactic.BVDecide.BVCheck

This modules provides the implementation of bv_check.

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

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

Instances For
    source
    def Lean.Elab.Tactic.BVDecide.BVCheck.mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) :
    TermElabM Meta.Tactic.BVDecide.TacticContext
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.BVCheck.bvCheck (g : MVarId) (ctx : Meta.Tactic.BVDecide.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"
      Instances For
        source
        def Lean.Elab.Tactic.BVDecide.BVCheck.evalBvCheck :
        Tactic
        Instances For