This module provides the implementation of the bv_decide frontend itself.

def Lean.Elab.Tactic.BVDecide.evalBvDecide : Tactic

Equations

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