From 6046f62d1874d12c00d99dffdf330ba738718799 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Wed, 20 May 2026 20:50:26 +0000 Subject: [PATCH] =?UTF-8?q?chore:=20bump=20mathlib=20to=205feb5ab:=20feat(?= =?UTF-8?q?Data/NNReal):=20`nnabs=20n=20=3D=20n`=20for=20`n=20:=20?= =?UTF-8?q?=E2=84=95`=20(#39577)=20(2026-05-20)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lake-manifest.json | 10 +++++----- lakefile.toml | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index ca8591cf3..6cea350ad 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "rev": "5feb5abb2b8105a13ef2ab9235ccf403c508d674", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5", + "inputRev": "5feb5abb2b8105a13ef2ab9235ccf403c508d674", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "4ee56e687ce2b9b51b097bfa65947a499da0c453", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 4169d4b8e..524239853 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5" +rev = "5feb5abb2b8105a13ef2ab9235ccf403c508d674" [[lean_lib]] name = "Cslib"