Provides the logic for reifying BitVec expressions.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr : Type

A reified version of an Expr representing a BVExpr.

• width : Nat
• bvExpr : Std.Tactic.BVDecide.BVExpr self.width

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkEvalExpr (w : Nat) (expr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

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

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)

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

Reify an Expr that's a BitVec.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.ofAtom (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.ofOrAtom (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstLikeReflection (distance : Nat) (innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName : Lake.Name) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.rotateReflection (x : Lean.Expr) (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (rotateOp : Nat → Std.Tactic.BVDecide.BVUnOp) (rotateOpName : Lake.Name) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstReflection (x : Lean.Expr) (β : Lean.Expr) (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName : Lake.Name) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftReflection (x : Lean.Expr) (β : Lean.Expr) (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (shiftOp : {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m) (shiftOpName : Lake.Name) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryReflection (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (op : Std.Tactic.BVDecide.BVBinOp) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryCongrProof (lhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (congrThm : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryReflection (innerExpr : Lean.Expr) (op : Std.Tactic.BVDecide.BVUnOp) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryCongrProof (inner : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (innerExpr : Lean.Expr) (congrProof : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.goBvLit (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

Equations

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