Provides the logic for reifying BitVec expressions.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkEvalExpr (w : Nat) (expr : Expr) : M 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.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkBVRefl (w : Nat) (expr : Expr) : Expr

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr

Register e as an atom of width that might potentially be synthetic.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.getNatOrBvValue? (ty expr : Expr) : M (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.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.bitVecAtom (x : Expr) (synthetic : Bool) : M (Option ReifiedBVExpr)

Construct an uninterpreted BitVec atom from x, potentially synthetic.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkBVConst {w : Nat} (val : BitVec w) : M ReifiedBVExpr

Build a reified version of the constant val.

Equations

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