Merge pull request #80 from gebner/bump220818

chore: update toolchain
main
Henrik Böving 2022-08-18 13:41:59 +02:00 committed by GitHub
commit b18f4e52ed
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 5 additions and 5 deletions

View File

@ -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 ⟩

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-08-09
leanprover/lean4:nightly-2022-08-18