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.

Equations

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

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.

Equations

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

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.

Equations

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