Provides the logic for reifying expressions consisting of predicates over BitVecs.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred : Type

A reified version of an Expr representing a BVPred.

• bvPred : Std.Tactic.BVDecide.BVPred

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvPred.eval atomsAssignment = originalBVPredExpr.

• expr : Lean.Expr

  A cache for toExpr bvPred

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred)

Reify an Expr that is a proof of a predicate about BitVec.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of.binaryReflection (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (pred : Std.Tactic.BVDecide.BVBinPred) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred)

Equations

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