We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 0a77d92 commit 8360f7fCopy full SHA for 8360f7f
Blase/Blase/Fast/MBA.lean
@@ -728,7 +728,7 @@ theorem BitVec.sub_distrib_add (x y z : BitVec w) :
728
omega
729
730
731
-attribute [bv_mba_preprocess] BitVec.sub_toAdd
+attribute [bv_mba_preprocess] BitVec.sub_eq_add_neg
732
733
@[bv_mba_preprocess]
734
theorem BitVec.ofNat_eq_ofInt (n w : Nat) :
LeanMLIR/LeanMLIR/Tactic.lean
@@ -47,7 +47,7 @@ attribute [simp_denote]
47
Expr.op_castPureToEff Expr.args_castPureToEff
48
/- Effect massaging -/
49
EffectKind.liftEffect_rfl
50
- Id.pure_eq Id.bind_eq id_eq
+ Id.pure_eq' Id.bind_eq' id_eq
51
pure_bind
52
cast_eq
53
-- Valuation append & accesses
0 commit comments