Provides the logic for reifying BitVec
expressions.
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
Instances For
def
Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.mkAtom
(e : Expr)
(width : Nat)
(synthetic : Bool)
:
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.
Instances For
Construct an uninterpreted BitVec
atom from x
, potentially synthetic
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build a reified version of the constant val
.
Equations
- One or more equations did not get rendered due to their size.