From 5e5bbe6ffb2585ee98227cbd407fe48d8e58f328 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 12 Dec 2021 13:33:24 +0100
Subject: [PATCH] chore: Update lean toolchain

---
 DocGen4/Hierarchy.lean | 2 +-
 DocGen4/Output.lean    | 7 ++++---
 lean-toolchain         | 2 +-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean
index 034a290..9f8a0d4 100644
--- a/DocGen4/Hierarchy.lean
+++ b/DocGen4/Hierarchy.lean
@@ -51,7 +51,7 @@ def getName : Hierarchy → Name
 def getChildren : Hierarchy → HierarchyMap
 | node _ c => c
 
-partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := do
+partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
   let hn := h.getName
   let mut cs := h.getChildren
   if getDepth hn ≥ getDepth n then
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 9c1f124..a11618f 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -26,9 +26,10 @@ def getResult : HtmlM AnalyzerResult := do (←read).result
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base
 
-def nameToPath (n : Name) : String := do
-  let parts := n.components.map Name.toString
-  return (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+def nameToPath (n : Name) : String :=
+    (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+  where
+    parts := n.components.map Name.toString
 
 partial def moduleListAux (h : Hierarchy) : HtmlM Html := do
   if h.getChildren.toList.length == 0 then
diff --git a/lean-toolchain b/lean-toolchain
index 45db7af..8b6c918 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2021-12-10
+leanprover/lean4:nightly-2021-12-12