From e5b44f1cdfcf19ae748dcb30b89ca5fbdd0ec9e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 16 Apr 2023 01:30:21 +0200
Subject: [PATCH] chore: update toolchain

---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 lean-toolchain     | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index d142855..442099d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,7 +10,7 @@
   {"git":
    {"url": "https://github.com/leanprover/lake",
     "subDir?": null,
-    "rev": "9e00151251d3e550f1ef4b24e59fd0d0419b0602",
+    "rev": "f120dbcaf8dafe864a5a4c28b34500352dbf1e60",
     "name": "lake",
     "inputRev?": "master"}},
   {"git":
@@ -28,6 +28,6 @@
   {"git":
    {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "0930d561409bc8b36551b22e85575009289e602e",
+    "rev": "be1f061688faa1dbb224773c54901661253fb4b8",
     "name": "UnicodeBasic",
     "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index d1d53d2..267bd15 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -71,7 +71,7 @@ library_facet docs (lib) : FilePath := do
 
   -- XXX: Workaround remove later
   let coreJob ← if h : docGen4Pkg.name = _package.name then
-    have : Fact (docGen4Pkg.name = _package.name) := Fact.mk h
+    have : PackageName docGen4Pkg _package.name := ⟨h⟩
     let job := fetch <| docGen4Pkg.target `coreDocs
     job
   else
diff --git a/lean-toolchain b/lean-toolchain
index dfc7b2c..3c7418e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-03-15
+leanprover/lean4:nightly-2023-04-11