chore: update mathlib (#688)

opencompl · Oct 10, 2024 · 29bf316 · 29bf316
1 parent 8a8f066
commit 29bf316
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 10 deletions.
diff --git a/SSA/Experimental/Bits/Fast/Circuit.lean b/SSA/Experimental/Bits/Fast/Circuit.lean
@@ -548,7 +548,7 @@ theorem card_varsFinset_assignVars_lt [DecidableEq α] [DecidableEq β]
           use ha'
           simp only [mem_varsFinset.1 ha', dite_true]
           split at hb₂
-          · simpa [*, eq_comm] using hb₂
+          · simp_all
           · simp at hb₂
    _ ≤ _ := Finset.card_image_le
 

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -230,15 +230,15 @@ def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
       simp only [BitVec.sdiv, lt_add_iff_pos_left, add_pos_iff, zero_lt_one,
         or_true, msb_one, neg_eq]
       by_cases h : a.msb <;> simp [h]
-      · rw [BitVec.udiv_eq_zero]
+      · rw [← BitVec.udiv_eq, BitVec.udiv_eq_zero]
         apply BitVec.gt_one_of_neq_0_neq_1
         · rw [neg_ne_iff_ne_neg]
           simp only [_root_.neg_zero]
           assumption
         · rw [neg_ne_iff_ne_neg]
           rw [← negOne_eq_allOnes] at hao
           assumption
-      · rw [BitVec.udiv_eq_zero]
+      · rw [← BitVec.udiv_eq, BitVec.udiv_eq_zero]
         apply BitVec.gt_one_of_neq_0_neq_1 <;> assumption
 
 def sdiv_one_one : BitVec.sdiv 1#w 1#w = 1#w := by

diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -130,7 +130,7 @@ def eg₀ : Com Simple (Ctxt.ofList []) .pure .int :=
   }]
 
 def eg₀val := Com.denote eg₀ Ctxt.Valuation.nil
-/-- info: 8 -/
+/-- info: 8#32 -/
 #guard_msgs in #eval eg₀val
 
 open MLIR AST MLIR2Simple in

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9080a05cbfaea73ee81d426c18a9f69fa0d040d1",
+   "rev": "b2f67acc31c54be78517f343e8d84447801dbe92",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16b29255b0f85e924cd32a6d5b5a275848b47903",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e",
+   "rev": "ccfb9511e1875f89123857f93865228ade8d0cef",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-10-08",
+   "inputRev": "nightly-testing-2024-10-09",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",

diff --git a/lakefile.toml b/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-10-08"
+rev = "nightly-testing-2024-10-09"
 
 [[require]]
 name = "Cli"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-08
+leanprover/lean4:nightly-2024-10-09