HepLean Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.SatAtBVLogical

This module is the main entry point for reifying BitVec problems with boolean substructure. Given some proof h : exp = true where exp is a BitVec problem with boolean substructure, it returns a SatAtBVLogical, containing the reified version as well as a proof that the reified version must be equal to true.

source
def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.of (h : Lean.Expr) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Reify an Expr that is a proof of some boolean structure on top of predicates about BitVecs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.and (x y : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) :
    Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical

    Logical conjunction of two ReifiedBVLogical.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.proveFalse (x : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) (h : Lean.Expr) :
      Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

      Given a proof that x.expr.Unsat, produce a proof of False.

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