step 1

LeanSAT/Reflect/Tactics/Normalize/Bool.lean

@@ -19,11 +19,7 @@ attribute [bv_normalize] Bool.true_and
 attribute [bv_normalize] Bool.and_false
 attribute [bv_normalize] Bool.false_and
 attribute [bv_normalize] beq_self_eq_true'
-attribute [bv_normalize] Bool.not_beq_false
-attribute [bv_normalize] Bool.not_beq_true
-attribute [bv_normalize] Bool.beq_true
 attribute [bv_normalize] Bool.true_beq
-attribute [bv_normalize] Bool.beq_false
 attribute [bv_normalize] Bool.false_beq
 attribute [bv_normalize] Bool.beq_not_self
 attribute [bv_normalize] Bool.not_beq_self

LeanSAT/Reflect/Tactics/Normalize/Equal.lean

@@ -8,9 +8,9 @@ import LeanSAT.Reflect.Tactics.Attr
 namespace BVDecide
 namespace Normalize
 
-attribute [bv_normalize] Bool.beq_true
+attribute [bv_normalize] beq_true
 attribute [bv_normalize] Bool.true_beq
-attribute [bv_normalize] Bool.beq_false
+attribute [bv_normalize] beq_false
 attribute [bv_normalize] Bool.false_beq
 attribute [bv_normalize] beq_self_eq_true
 attribute [bv_normalize] beq_self_eq_true'

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "b24f8d9e82cf133812e74df1adb6d049de74eeb0",
+   "scope": "",
+   "rev": "141853159817b913f8da3da94c84f46f0a445bcd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-06-28
+leanprover/lean4:nightly-2024-07-03