This module provides the implementation of the bv_decide frontend itself.

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

• satExpr : SatAtBVLogical

  The reflected expression together with ways to prove things about it.

• unusedHypotheses : Std.HashSet Normalize.Hyp

  Set of unused hypotheses for diagnostic purposes.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.UnsatProver (α : Type) : Type

Equations

• Lean.Meta.Tactic.BVDecide.UnsatProver α = (Lean.MVarId → Lean.Meta.Tactic.BVDecide.ReflectionResult → Lean.Meta.Tactic.BVDecide.LemmaM (Except Lean.Meta.Tactic.BVDecide.CounterExample α))

def Lean.Meta.Tactic.BVDecide.UnsatProver.map {α β : Type} (f : α → β) (x : UnsatProver α) : UnsatProver β

Equations

• Lean.Meta.Tactic.BVDecide.UnsatProver.map f x g r = do let res ← x g r pure (Except.map f res)

def Lean.Meta.Tactic.BVDecide.reflectBV (g : MVarId) : ReifyM ReflectionResult

Equations

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

def Lean.Meta.Tactic.BVDecide.closeWithBVReflection {α : Type} (g : MVarId) (unsatProver : UnsatProver α) : ReifyM (Except CounterExample α)

Equations

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