Provides the logic for reifying predicates on BitVec.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.boolAtom (origExpr : Expr) : M (Option ReifiedBVPred)

Construct an uninterpreted Bool atom from origExpr.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : Std.Tactic.BVDecide.BVBinPred) (origExpr : Expr) : M (Option ReifiedBVPred)

Construct the reified version of applying the predicate in pred to lhs and rhs. This function assumes that lhsExpr and rhsExpr are the corresponding expressions to lhs and rhs.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) (origExpr : Expr) : M ReifiedBVPred

Construct the reified version of BitVec.getLsbD subExpr idx. This function assumes that subExpr is the expression corresponding to sub.