From 9dc1889de69935143f232b240c1475c6cd00eac3 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 18 Aug 2022 11:31:18 +0200 Subject: [PATCH] chore: update toolchain --- DocGen4/Output/DocString.lean | 8 ++++---- lean-toolchain | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 971d066..a3bfd88 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -128,7 +128,7 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme |>.insert "class" "markdown-heading" let newContents := (← contents.mapM (λ c => match c with - | Content.Element e => (modifyElement e).map (Content.Element) + | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c)) |>.push (Content.Character " ") |>.push (Content.Element anchor) @@ -138,8 +138,8 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme def extendAnchor (el : Element) : HtmlM Element := do match el with | Element.Element name attrs contents => - let newAttrs ← match (attrs.find? "href").map extendLink with - | some href => href.map (attrs.insert "href") + let newAttrs ← match attrs.find? "href" with + | some href => pure (attrs.insert "href" (← extendLink href)) | none => pure attrs pure ⟨ name, newAttrs, contents⟩ @@ -193,7 +193,7 @@ partial def modifyElement (element : Element) : HtmlM Element := -- recursively modify else let newContents ← contents.mapM λ c => match c with - | Content.Element e => (modifyElement e).map Content.Element + | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c pure ⟨ name, attrs, newContents ⟩ diff --git a/lean-toolchain b/lean-toolchain index f62cade..9618929 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-08-09 +leanprover/lean4:nightly-2022-08-18