Provides the logic for reifying BitVec expressions.

def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkEvalExpr (w : Nat) (expr : Expr) : ReifyM Expr

Build BVExpr.eval atoms expr where atoms is the assignment stored in the monad.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkBVRefl (w : Nat) (expr : Expr) : Expr

Equations

• Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkBVRefl w expr = Lean.mkApp2 (Lean.mkConst `Eq.refl [1]) (Lean.mkApp (Lean.mkConst `BitVec) (Lean.toExpr w)) expr

def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.getNatOrBvValue? (ty expr : Expr) : ReifyM (Option Nat)

Parse expr as a Nat or BitVec constant depending on ty.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkBVConst {w : Nat} (val : BitVec w) : ReifyM ReifiedBVExpr

Build a reified version of the constant val.

Equations

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