chore: update nightly

leanprover · Jul 5, 2024 · 2b7ae31 · 2b7ae31
1 parent ec1e572
commit 2b7ae31
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 11 deletions.
diff --git a/LeanSAT/AIG/CNF.lean b/LeanSAT/AIG/CNF.lean
@@ -55,7 +55,7 @@ theorem atomToCNF_eval :
     (atomToCNF output a).eval assign
       =
     (assign output == assign a) := by
-  simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, Bool.beq_true, Bool.beq_false,
+  simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, beq_true, beq_false,
     CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true]
   cases assign output <;> cases assign a <;> decide
 

diff --git a/LeanSAT/AIG/CachedLemmas.lean b/LeanSAT/AIG/CachedLemmas.lean
@@ -298,7 +298,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
       simp_all [denote_idx_const heq]
     . split
       . next hif =>
-        simp only [Bool.beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
+        simp only [beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
         rcases hif with ⟨⟨hifeq, hlinv⟩, hrinv⟩
         replace hifeq : input.lhs.ref = input.rhs.ref := by
           rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩

diff --git a/LeanSAT/Reflect/Tactics/Normalize/Bool.lean b/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

diff --git a/LeanSAT/Reflect/Tactics/Normalize/Equal.lean b/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'

diff --git a/lake-manifest.json b/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": "4e1d17623329b6a46bd6007f031d28119f59d0d1",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-06-28
+leanprover/lean4:nightly-2024-07-03
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,2 @@
		leanprover/lean4:nightly-2024-06-28
		leanprover/lean4:nightly-2024-07-03