From 2a4af2a27acdba2571daae58ef9d701274b1da05 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Wed, 17 Apr 2024 16:01:16 +0200 Subject: [PATCH 1/3] fix: `Mathlib.Data.Int.Basic` does not exist anymore Signed-off-by: Raito Bezarius --- Aegis/Aux/ZMod/HMul.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Aegis/Aux/ZMod/HMul.lean b/Aegis/Aux/ZMod/HMul.lean index fb16a8d..d2ef6ff 100644 --- a/Aegis/Aux/ZMod/HMul.lean +++ b/Aegis/Aux/ZMod/HMul.lean @@ -1,5 +1,4 @@ import Mathlib.Data.ZMod.Basic -import Mathlib.Data.Int.Basic namespace ZMod From 7eac627c649204888139f36656080bc102cadebf Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Wed, 17 Apr 2024 16:01:26 +0200 Subject: [PATCH 2/3] fix: `ZMod.val_nat_cast` -> `ZMod.val_natCast` Signed-off-by: Raito Bezarius --- Aegis/Aux/ZMod/DivMod.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Aegis/Aux/ZMod/DivMod.lean b/Aegis/Aux/ZMod/DivMod.lean index 28e9f7d..e6750dd 100644 --- a/Aegis/Aux/ZMod/DivMod.lean +++ b/Aegis/Aux/ZMod/DivMod.lean @@ -29,4 +29,4 @@ theorem val_nmod (hb : b ≠ 0) : (nmod a b).val = a.val % b.val := by intro h rw [val_eq_zero] at h contradiction - rw [ZMod.val_nat_cast, Nat.mod_eq_of_lt (lt_trans (Nat.mod_lt _ this) b.val_lt)] + rw [ZMod.val_natCast, Nat.mod_eq_of_lt (lt_trans (Nat.mod_lt _ this) b.val_lt)] From c47d5085701e0052ea590cd56e36bfd8fcd37ed7 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Wed, 17 Apr 2024 16:01:56 +0200 Subject: [PATCH 3/3] chore: upgrade to Lean 4.7.0 and newer dependencies Signed-off-by: Raito Bezarius --- lake-manifest.json | 20 ++++++++++---------- lean-toolchain | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index d90ab47..c86bd3b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,16 +4,16 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", + "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "fd760831487e6835944e7eeed505522c9dd47563", + "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,25 +22,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b", + "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "16cae05860b208925f54e5581ec5fd264823440c", + "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.29", + "inputRev": "v0.0.30", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec", + "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f", + "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "5925ea9ba2855f58fdde427199200d511e1855fc", + "rev": "e4721ccdbd69b0124f1c947b821033ae422b4789", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index 5026204..9ad3040 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0 +leanprover/lean4:v4.7.0