This module provides the implementation of the bv_decide frontend itself.

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

The result of calling bv_decide.

• cegarCert : CegarCert

def Lean.Meta.Tactic.BVDecide.bvDecide' (target : Normalize.Target) (ctx : TacticContext) : Grind.GrindM (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 (target : Normalize.Target) (ctx : TacticContext) : Grind.GrindM 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.