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

def
Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.lratChecker
(cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext)
(bvExpr : Std.Tactic.BVDecide.BVLogicalExpr)
:

Prepare an `Expr`

that proves `bvExpr.unsat`

using `ofReduceBool`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

def
Lean.Elab.Tactic.BVDecide.Frontend.BVCheck.bvCheck
(g : Lean.MVarId)
(cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext)
:

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.