Provides the logic for reifying BitVec expressions.

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

Register e as an atom of width width.

Equations

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

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

Construct an uninterpreted BitVec atom from x.

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) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr

Build a reified version of the constant val.

Equations

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