Provides the logic for reifying predicates on BitVec.

def Lean.Meta.Tactic.BVDecide.ReifiedBVPred.mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : Std.Tactic.BVDecide.BVBinPred) (origExpr : Expr) : ReifyM (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.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifiedBVPred.mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) (origExpr : Expr) : ReifyM ReifiedBVPred

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

Equations

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