This module provides the implementation of the bv_decide frontend itself.

structure Lean.Meta.Tactic.BVDecide.Result : Type

The result of calling bv_decide.

• lratCert : Option LratCert

  If the normalization step was not enough to solve the goal this contains the LRAT proof certificate.

def Lean.Meta.Tactic.BVDecide.bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result)

Try to close g using a bitblaster. Return either a CounterExample if one is found or a Result if g is proven.

Equations

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

def Lean.Meta.Tactic.BVDecide.bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result

Call bvDecide' and throw a pretty error if a counter example ends up being produced.

Equations

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