style: Lean 4 compiler style in output

DocGen4/Output/Base.lean

@@ -66,10 +66,10 @@ def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) :
   ReaderT.run x ctx |>.run baseCtx |>.run
 
 instance [Monad m] : MonadLift HtmlM (HtmlT m) where
-  monadLift x := do pure <| x.run (←readThe SiteContext) (←readThe SiteBaseContext)
+  monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
 
 instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
-  monadLift x := do pure <| x.run (←readThe SiteBaseContext)
+  monadLift x := do return x.run (← readThe SiteBaseContext)
 
 /--
 Obtains the root URL as a relative one to the current depth.
@@ -81,11 +81,11 @@ def getRoot : BaseHtmlM String := do
   let d <- SiteBaseContext.depthToRoot <$> read
   return (go d)
 
-def getHierarchy : BaseHtmlM Hierarchy := do pure (←read).hierarchy
+def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy
-def getCurrentName : BaseHtmlM (Option Name) := do pure (←read).currentName
+def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
-def getResult : HtmlM AnalyzerResult := do pure (←read).result
+def getResult : HtmlM AnalyzerResult := do return (← read).result
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure <| (←read).sourceLinker module range
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
-def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
+def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
 
 /--
 If a template is meant to be extended because it for example only provides the
@@ -102,20 +102,20 @@ Returns the doc-gen4 link to a module name.
 -/
 def moduleNameToLink (n : Name) : BaseHtmlM String := do
   let parts := n.components.map Name.toString
-  pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+  return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 /--
 Returns the HTML doc-gen4 link to a module name.
 -/
 def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
-  pure <a href={←moduleNameToLink module}>{module.toString}</a>
+  return <a href={← moduleNameToLink module}>{module.toString}</a>
 
 /--
 Returns the LeanInk link to a module name.
 -/
 def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
   let parts := "src" :: n.components.map Name.toString
-  pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+  return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 /--
 Returns the path to the HTML file that contains information about a module.
@@ -158,13 +158,13 @@ Returns the doc-gen4 link to a declaration name.
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
   let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
-  pure <| (←moduleNameToLink module) ++ "#" ++ name.toString
+  return (← moduleNameToLink module) ++ "#" ++ name.toString
 
 /--
 Returns the HTML doc-gen4 link to a declaration name.
 -/
 def declNameToHtmlLink (name : Name) : HtmlM Html := do
-  pure <a href={←declNameToLink name}>{name.toString}</a>
+  return <a href={← declNameToLink name}>{name.toString}</a>
 
 /--
 Returns the LeanInk link to a declaration name.
@@ -172,14 +172,14 @@ Returns the LeanInk link to a declaration name.
 def declNameToInkLink (name : Name) : HtmlM String := do
   let res ← getResult
   let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
-  pure <| (←moduleNameToInkLink module) ++ "#" ++ name.toString
+  return (← moduleNameToInkLink module) ++ "#" ++ name.toString
 
 /--
 Returns the HTML doc-gen4 link to a declaration name with "break_within"
 set as class.
 -/
 def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
-  pure <a class="break_within" href={←declNameToLink name}>{name.toString}</a>
+  return <a class="break_within" href={← declNameToLink name}>{name.toString}</a>
 
 /--
 In Lean syntax declarations the following pattern is quite common:
@@ -207,8 +207,8 @@ to as much information as possible.
 -/
 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   match i with
-  | .text t => pure #[Html.escape t]
+  | .text t => return #[Html.escape t]
-  | .append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
+  | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[]
   | .tag a t =>
     match a.info.val.info with
     | Info.ofTermInfo i =>
@@ -222,11 +222,11 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
           | .text t =>
             let (front, t, back) := splitWhitespaces <| Html.escape t
             let elem := <a href={← declNameToLink name}>{t}</a>
-            pure #[Html.text front, elem, Html.text back]
+            return #[Html.text front, elem, Html.text back]
           | _ =>
-            pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
+            return #[<a href={← declNameToLink name}>[← infoFormatToHtml t]</a>]
         else
-         pure #[<span class="fn">[←infoFormatToHtml t]</span>]
+         return #[<span class="fn">[← infoFormatToHtml t]</span>]
       | .sort _ =>
         match t with
         | .text t =>
@@ -234,15 +234,15 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
           let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
           if rest != [] then
             rest := " " :: rest
-          pure #[sortLink, Html.text <| String.join rest]
+          return #[sortLink, Html.text <| String.join rest]
         | _ =>
-          pure #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
+          return #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
       | _ =>
-         pure #[<span class="fn">[←infoFormatToHtml t]</span>]
+         return #[<span class="fn">[← infoFormatToHtml t]</span>]
-    | _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
+    | _ => return #[<span class="fn">[← infoFormatToHtml t]</span>]
 
 def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
-  pure #[
+  return #[
     <meta charset="UTF-8"/>,
     <meta name="viewport" content="width=device-width, initial-scale=1"/>,
     <link rel="stylesheet" href={s!"{← getRoot}style.css"}/>,

DocGen4/Output/Definition.lean

@@ -12,7 +12,7 @@ open Lean Widget
 def equationLimit : Nat := 200
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
-  pure <li class="equation">[←infoFormatToHtml c]</li>
+  return <li class="equation">[← infoFormatToHtml c]</li>
 
 /--
 Attempt to render all `simp` equations for this definition. At a size
@@ -23,9 +23,9 @@ defined in `equationLimit` we stop trying since they:
 def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
-    let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)
+    let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit)
     if equationsHtml.size ≠ filteredEquationsHtml.size then
-      pure #[
+      return #[
         <details>
           <summary>Equations</summary>
           <ul class="equations">
@@ -35,7 +35,7 @@ def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
         </details>
       ]
     else
-      pure #[
+      return #[
         <details>
           <summary>Equations</summary>
           <ul class="equations">
@@ -44,7 +44,7 @@ def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
         </details>
       ]
   else
-    pure #[]
+    return #[]
 
 end Output
 end DocGen4

DocGen4/Output/DocString.lean

@@ -23,7 +23,7 @@ namespace Output
 
 /--
   Similar to `Stirng.split` in Lean core, but keeps the separater.
-  e.g. `splitAround "a,b,c" (λ c => c = ',') = ["a", ",", "b", ",", "c"]`
+  e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
 -/
 def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
 
@@ -81,15 +81,15 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
         match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
         | some info =>
           declNameToLink info.getName
-        | _ => pure none
+        | _ => return none
-      | _ => pure none
+      | _ => return none
   else
-    pure none
+    return none
   where
     -- check if two names have the same ending components
     sameEnd n1 n2 :=
       List.zip n1.componentsRev n2.componentsRev
-      |>.all λ ⟨a, b⟩ => a == b
+      |>.all fun ⟨a, b⟩ => a == b
 
 /--
   Extend links with following rules:
@@ -103,16 +103,16 @@ def extendLink (s : String)  : HtmlM String := do
   -- for intra doc links
   if s.startsWith "##" then
     if let some link ← nameToLink? (s.drop 2) then
-      pure link
+      return link
     else
       panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
   -- for id
   else if s.startsWith "#" then
-    pure s
+    return s
   -- for absolute and relative urls
   else if s.startsWith "http" then
-    pure s
+    return s
-  else pure ((←getRoot) ++ s)
+  else return ((← getRoot) ++ s)
 
 /-- Add attributes for heading. -/
 def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
@@ -127,12 +127,12 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme
       |>.insert "id" id
       |>.insert "class" "markdown-heading"
     let newContents := (←
-      contents.mapM (λ c => match c with
+      contents.mapM (fun c => match c with
       | Content.Element e => return Content.Element (← modifyElement e)
       | _ => pure c))
       |>.push (Content.Character " ")
       |>.push (Content.Element anchor)
-    pure ⟨ name, newAttrs, newContents⟩
+    return ⟨ name, newAttrs, newContents⟩
 
 /-- Extend anchor links. -/
 def extendAnchor (el : Element) : HtmlM Element := do
@@ -141,7 +141,7 @@ def extendAnchor (el : Element) : HtmlM Element := do
     let newAttrs ← match attrs.find? "href" with
     | some href => pure (attrs.insert "href" (← extendLink href))
     | none => pure attrs
-    pure ⟨ name, newAttrs, contents⟩
+    return ⟨ name, newAttrs, contents⟩
 
 /-- Automatically add intra documentation link for inline code span. -/
 def autoLink (el : Element) : HtmlM Element := do
@@ -153,27 +153,27 @@ def autoLink (el : Element) : HtmlM Element := do
       | Content.Character s =>
         newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
       | _ => newContents := newContents.push c
-    pure ⟨ name, attrs, newContents ⟩
+    return ⟨ name, attrs, newContents ⟩
   where
     linkify s := do
       let link? ← nameToLink? s
       match link? with
       | some link =>
         let attributes := Lean.RBMap.empty.insert "href" link
-        pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
+        return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
       | none =>
-        let sHead := s.dropRightWhile (λ c => c ≠ '.')
+        let sHead := s.dropRightWhile (· != '.')
-        let sTail := s.takeRightWhile (λ c => c ≠ '.')
+        let sTail := s.takeRightWhile (· != '.')
         let link'? ← nameToLink? sTail
         match link'? with
         | some link' =>
           let attributes := Lean.RBMap.empty.insert "href" link'
-          pure [
+          return [
             Content.Character sHead,
             Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
           ]
         | none =>
-          pure [Content.Character s]
+          return [Content.Character s]
     unicodeToSplit (c : Char) : Bool :=
       charInGeneralCategory c GeneralCategory.separator ||
       charInGeneralCategory c GeneralCategory.other
@@ -192,19 +192,18 @@ partial def modifyElement (element : Element) : HtmlM Element :=
       autoLink el
     -- recursively modify
     else
-      let newContents ← contents.mapM λ c => match c with
+      let newContents ← contents.mapM fun c => match c with
         | Content.Element e => return Content.Element (← modifyElement e)
         | _ => pure c
-      pure ⟨ name, attrs, newContents ⟩
+      return ⟨ name, attrs, newContents ⟩
 
 /-- Convert docstring to Html. -/
 def docStringToHtml (s : String) : HtmlM (Array Html) := do
   let rendered := CMark.renderHtml s
   match manyDocument rendered.mkIterator with
   | Parsec.ParseResult.success _ res =>
-    res.mapM λ x => do
+    res.mapM fun x => do return Html.text <| toString (← modifyElement x)
-      pure (Html.text <| toString (← modifyElement x))
+  | _ => return #[Html.text rendered]
-  | _ => pure #[Html.text rendered]
 
 end Output
 end DocGen4

DocGen4/Output/FoundationalTypes.lean

@@ -28,7 +28,7 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
       <p><code>Prop</code> is notation for <code>Sort 0</code>.</p>    
       {← instancesForToHtml `_builtin_prop}
     
-      <h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"Π a : α, β a"}</code></h2>
+      <h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"(a : α) → β a"}</code></h2>
       <p>The type of dependent functions is known as a pi type.
       Non-dependent functions and implications are a special case.</p>
       <p>Note that these can also be written with the alternative notations:</p>
@@ -39,13 +39,12 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
       </ul>
       <p>Lean also permits ASCII-only spellings of the three variants:</p>
       <ul>
-      <li><code>Pi a : A, B a</code> for <code>{"Π a : α, β a"}</code></li>
       <li><code>forall a : A, B a</code> for <code>{"∀ a : α, β a"}</code></li>
       <li><code>(a : A) -&gt; B a</code>, for <code>(a : α) → β a</code></li>
       <li><code>A -&gt; B</code>, for <code>α → β</code></li>
       </ul>
       <p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
-      <code>{"λ α β, α → β"}</code>.</p>    
+      <code>{"fun α β, α → β"}</code>.</p>    
       -- TODO: instances for pi types 
     </main>
 

DocGen4/Output/Inductive.lean

@@ -33,7 +33,7 @@ def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
 
 def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
-  pure #[constructorsHtml]
+  return #[constructorsHtml]
 
 end Output
 end DocGen4

DocGen4/Output/Module.lean

@@ -36,9 +36,9 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   let inner := <span class="fn">[nodes]</span>
   let html := Html.element "span" false #[("class", "decl_args")] #[inner]
   if implicit then
-    pure <span class="impl_arg">{html}</span>
+    return <span class="impl_arg">{html}</span>
   else
-    pure html
+    return html
 
 /--
 Render the structures this structure extends from as HTML so it can be
@@ -55,7 +55,7 @@ def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
       let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
       parents := parents.push html
     nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
-  pure nodes
+  return nodes
 
 /--
 Render the general header of a declaration containing its declaration type
@@ -81,7 +81,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
 
   nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
   nodes := nodes.push <div class="decl_type">[← infoFormatToHtml doc.getType]</div>
-  pure <div class="decl_header"> [nodes] </div>
+  return <div class="decl_header"> [nodes] </div>
 
 /--
 The main entry point for rendering a single declaration inside a given module.
@@ -168,15 +168,15 @@ Returns the list of all imports this module does.
 -/
 def getImports (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  pure <| res.moduleInfo.find! module |>.imports
+  return res.moduleInfo.find! module |>.imports
 
 /--
 Sort the list of all modules this one is importing, linkify it
 and return the HTML.
 -/
 def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
-  let imports := (←getImports moduleName) |>.qsort Name.lt
+  let imports := (← getImports moduleName).qsort Name.lt
-  imports.mapM (λ i => do pure <li>{←moduleToHtmlLink i}</li>)
+  imports.mapM (fun i => do return <li>{← moduleToHtmlLink i}</li>)
 
 /--
 Render the internal nav bar (the thing on the right on all module pages).
@@ -205,7 +205,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
 The main entry point to rendering the HTML for an entire module.
 -/
 def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
-  let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
+  let memberDocs ← module.members.mapM (moduleMemberToHtml module.name ·)
   let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
   templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
     ← internalNav memberNames module.name,

DocGen4/Output/Navbar.lean

@@ -14,7 +14,7 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : BaseHtmlM Html := do
-  pure <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
+  return <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
     <a href={← moduleNameToLink file}>{file.getString!}</a>
   </div>
 
@@ -23,11 +23,11 @@ Build the HTML tree representing the module hierarchy.
 -/
 partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
   let children := Array.mk (h.getChildren.toList.map Prod.snd)
-  let dirs := children.filter (λ c => c.getChildren.toList.length != 0)
+  let dirs := children.filter (fun c => c.getChildren.toList.length != 0)
-  let files := children.filter (λ c => Hierarchy.isFile c ∧ c.getChildren.toList.length = 0)
+  let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0)
     |>.map Hierarchy.getName
-  let dirNodes ← (dirs.mapM moduleListDir)
+  let dirNodes ← dirs.mapM moduleListDir
-  let fileNodes ← (files.mapM moduleListFile)
+  let fileNodes ← files.mapM moduleListFile
   let moduleLink ← moduleNameToLink h.getName
   let summary :=
     if h.isFile then
@@ -50,7 +50,7 @@ def moduleList : BaseHtmlM Html := do
   let mut list := Array.empty
   for (_, cs) in hierarchy.getChildren do
     list := list.push <| ← moduleListDir cs
-  pure <div class="module_list">[list]</div>
+  return <div class="module_list">[list]</div>
 
 /--
 The main entry point to rendering the navbar on the left hand side.

DocGen4/Output/SourceLinker.lean

@@ -25,11 +25,11 @@ def getGithubBaseUrl (gitUrl : String) : String := Id.run do
   if url.startsWith "git@" then
     url := url.drop 15
     url := url.dropRight 4
-    pure s!"https://github.com/{url}"
+    return s!"https://github.com/{url}"
   else if url.endsWith ".git" then
-    pure <| url.dropRight 4
+    return url.dropRight 4
   else
-    pure url
+    return url
 
 /--
 Obtain the Github URL of a project by parsing the origin remote.
@@ -38,7 +38,7 @@ def getProjectGithubUrl : IO String := do
   let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
   if out.exitCode != 0 then
     throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
+  return out.stdout.trimRight
 
 /--
 Obtain the git commit hash of the project that is currently getting analyzed.
@@ -47,7 +47,7 @@ def getProjectCommit : IO String := do
   let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
   if out.exitCode != 0 then
     throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
+  return out.stdout.trimRight
 
 /--
 Given a lake workspace with all the dependencies as well as the hash of the
@@ -63,12 +63,12 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
   gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
   let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile
       |>.run (Lake.MonadLog.eio .normal)
-      |>.toIO (λ _ => IO.userError "Failed to load lake manifest")
+      |>.toIO (fun _ => IO.userError "Failed to load lake manifest")
   for pkg in manifest.entryArray do
     if let  .git _ url rev .. := pkg then
       gitMap := gitMap.insert pkg.name (getGithubBaseUrl url, rev)
 
-  pure λ module range =>
+  return fun module range =>
     let parts := module.components.map Name.toString
     let path := (parts.intersperse "/").foldl (· ++ ·) ""
     let root := module.getRoot

DocGen4/Output/Structure.lean

@@ -45,7 +45,7 @@ def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
         </ul>
         <li class="structure_ext_ctor">)</li>
       </ul>)
-  pure #[structureHtml]
+  return #[structureHtml]
 
 end Output
 end DocGen4

DocGen4/Output/Template.lean

@@ -16,7 +16,7 @@ The HTML template used for all pages.
 -/
 def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
   let moduleConstant :=
-    if let some module := (←getCurrentName) then
+    if let some module := ← getCurrentName then
       #[<script>{s!"const MODULE_NAME={String.quote module.toString};"}</script>]
     else
       #[]

DocGen4/Output/ToHtmlFormat.lean

@@ -29,7 +29,7 @@ instance : Coe String Html :=
 namespace Html
 
 def attributesToString (attrs : Array (String × String)) :String :=
-  attrs.foldl (λ acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
+  attrs.foldl (fun acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
 
 -- TODO: Termination proof
 partial def toStringAux : Html → String
@@ -60,7 +60,7 @@ def escapePairs : Array (String × String) :=
   ]
 
 def escape (s : String) : String :=
-  escapePairs.foldl (λ acc (o, r) => acc.replace o r) s
+  escapePairs.foldl (fun acc (o, r) => acc.replace o r) s
 
 end Html
 

DocGen4/Output/ToJson.lean

@@ -36,11 +36,11 @@ structure JsonIndex where
 
 instance : ToJson JsonIndex where
   toJson idx := Id.run do
-    let jsonDecls := Json.mkObj <| idx.declarations.map (λ (k, v) => (k, toJson v))
+    let jsonDecls := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
-    let jsonInstances := Json.mkObj <| idx.instances.toList.map (λ (k, v) => (k, toJson v))
+    let jsonInstances := Json.mkObj <| idx.instances.toList.map (fun (k, v) => (k, toJson v))
-    let jsonImportedBy := Json.mkObj <| idx.importedBy.toList.map (λ (k, v) => (k, toJson v))
+    let jsonImportedBy := Json.mkObj <| idx.importedBy.toList.map (fun (k, v) => (k, toJson v))
-    let jsonModules := Json.mkObj <| idx.modules.map (λ (k, v) => (k, toJson v))
+    let jsonModules := Json.mkObj <| idx.modules.map (fun (k, v) => (k, toJson v))
-    let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (λ (k, v) => (k, toJson v))
+    let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (fun (k, v) => (k, toJson v))
     let finalJson := Json.mkObj [
       ("declarations", jsonDecls),
       ("instances", jsonInstances),
@@ -48,12 +48,12 @@ instance : ToJson JsonIndex where
       ("modules", jsonModules),
       ("instancesFor", jsonInstancesFor)
     ]
-    pure finalJson
+    return finalJson
 
 def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do
   let mut index := index
   let newModule := (module.name, ← moduleNameToLink (String.toName module.name))
-  let newDecls := module.declarations.map (λ d => (d.name, d))
+  let newDecls := module.declarations.map (fun d => (d.name, d))
   index := { index with
     modules := newModule :: index.modules
     declarations := newDecls ++ index.declarations
@@ -72,14 +72,14 @@ def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM Js
     let mut impBy := index.importedBy.findD imp #[]
     impBy := impBy.push module.name
     index := { index with importedBy := index.importedBy.insert imp impBy }
-  pure index
+  return index
 
 def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
   let name := info.getName.toString
   let doc := info.getDocString.getD ""
   let docLink ← declNameToLink info.getName
   let sourceLink ← getSourceUrl module info.getDeclarationRange
-  pure { name, doc, docLink, sourceLink }
+  return { name, doc, docLink, sourceLink }
 
 def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
     let mut jsonDecls := []
@@ -99,6 +99,6 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
       instances,
       imports := module.imports.map Name.toString
     }
-    pure <| ToJson.toJson jsonMod
+    return ToJson.toJson jsonMod
 
 end DocGen4.Output