Provides the logic for reifying predicates on BitVec.

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

Construct an uninterpreted Bool atom from t.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkBinPred (lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (lhsExpr rhsExpr : Lean.Expr) (pred : Std.Tactic.BVDecide.BVBinPred) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.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.mkBinPred.congrThmofBinPred (pred : Std.Tactic.BVDecide.BVBinPred) : Lean.Name

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkBinPred.congrThmofBinPred Std.Tactic.BVDecide.BVBinPred.eq = `Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkBinPred.congrThmofBinPred Std.Tactic.BVDecide.BVBinPred.ult = `Std.Tactic.BVDecide.Reflect.BitVec.ult_congr

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.mkGetLsbD (sub : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (subExpr : Lean.Expr) (idx : Nat) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.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.