chore: bump toolchain, bye auto pure

DocGen4/IncludeStr.lean

@@ -19,7 +19,7 @@ syntax (name := includeStr) "include_str" str : term
         throwError s!"{str} is a directory"
       else
         let content ← FS.readFile path
-        return mkStrLit content
+        pure $ mkStrLit content
     else
       throwError s!"\"{str}\" does not exist as a file"
 

DocGen4/Load.lean

@@ -14,10 +14,10 @@ open Lean System Std IO
 
 def getLakePath : IO FilePath := do
   match (← IO.getEnv "LAKE") with
-  | some path => System.FilePath.mk path
+  | some path => pure $ System.FilePath.mk path
   | none =>
     let lakePath := (←findSysroot?) / "bin" / "lake"
-    lakePath.withExtension System.FilePath.exeExtension
+    pure $ lakePath.withExtension System.FilePath.exeExtension
 
 -- Modified from the LSP Server
 def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do

DocGen4/Output.lean

@@ -32,22 +32,22 @@ def getGithubBaseUrl : IO String := do
   if url.startsWith "git@" then
     url := url.drop 15
     url := url.dropRight 4
-    s!"https://github.com/{url}"
+    pure s!"https://github.com/{url}"
   else if url.endsWith ".git" then
-    url.dropRight 4
+    pure $ url.dropRight 4
   else
-    url
+    pure url
 
 def getCommit : 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
-  out.stdout.trimRight
+  pure out.stdout.trimRight
 
 def sourceLinker : IO (Name → Option DeclarationRange → String) := do
   let baseUrl ← getGithubBaseUrl
   let commit ← getCommit
-  return λ name range =>
+  pure λ name range =>
     let parts := name.components.map Name.toString
     let path := (parts.intersperse "/").foldl (· ++ ·) ""
     let r := name.getRoot

DocGen4/Output/Base.lean

@@ -25,17 +25,17 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName :=
 abbrev HtmlT := ReaderT SiteContext
 abbrev HtmlM := HtmlT Id
 
-def getRoot : HtmlM String := do (←read).root
+def getRoot : HtmlM String := do pure (←read).root
-def getResult : HtmlM AnalyzerResult := do (←read).result
+def getResult : HtmlM AnalyzerResult := do pure (←read).result
-def getCurrentName : HtmlM (Option Name) := do (←read).currentName
+def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do (←read).sourceLinker module range
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
 
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base
 
 def moduleNameToLink (n : Name) : HtmlM String := do
   let parts := n.components.map Name.toString
-  (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+  pure $ (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
   let parts := n.components.map Name.toString
@@ -53,7 +53,7 @@ end Static
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
   let module := res.moduleNames[res.name2ModIdx.find! name]
-  (←moduleNameToLink module) ++ "#" ++ name.toString
+  pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
 
 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
   let front := "".pushn ' ' (s.find (!Char.isWhitespace ·))
@@ -64,8 +64,8 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do
 
 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   match i with
-  | TaggedText.text t => return #[t]
+  | TaggedText.text t => pure #[t]
-  | TaggedText.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[]
+  | TaggedText.append tt => tt.foldlM (λ acc t => do pure $ acc ++ (←infoFormatToHtml t)) #[]
   | TaggedText.tag a t =>
     match a.info.val.info with
     | Info.ofTermInfo i =>
@@ -75,13 +75,13 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
          | TaggedText.text t =>
            let (front, t, back) := splitWhitespaces t
            let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t]
-           #[Html.text front, elem, Html.text back]
+           pure #[Html.text front, elem, Html.text back]
          | _ =>
            -- TODO: Is this ever reachable?
-           #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
+           pure #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
       | _ =>
-         #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+         pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
-    | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+    | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
 
 end Output
 end DocGen4

DocGen4/Output/Class.lean

@@ -8,11 +8,12 @@ open scoped DocGen4.Jsx
 open Lean
 
 def classInstanceToHtml (name : Name) : HtmlM Html := do
-  <li><a href={←declNameToLink name}>{name.toString}</a></li>
+  pure <li><a href={←declNameToLink name}>{name.toString}</a></li>
 
 def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
   let instancesHtml ← instances.mapM classInstanceToHtml
-  return <details «class»="instances">
+  pure
+    <details «class»="instances">
         <summary>Instances</summary>
         <ul>
           [instancesHtml]
@@ -20,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
     </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
 
 end Output
 end DocGen4

DocGen4/Output/ClassInductive.lean

@@ -7,7 +7,7 @@ namespace DocGen4
 namespace Output
 
 def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
-  (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
 
 end Output
 end DocGen4

DocGen4/Output/Definition.lean

@@ -7,26 +7,27 @@ open scoped DocGen4.Jsx
 open Lean Widget
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
-  <li «class»="equation">[←infoFormatToHtml c]</li>
+  pure <li «class»="equation">[←infoFormatToHtml c]</li>
 
 def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
-  if let some eqs ← i.equations then
+  if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
-    return <details>
+    pure
-      <summary>Equations</summary>
+      <details>
-      <ul «class»="equations">
+        <summary>Equations</summary>
-        [equationsHtml]
+        <ul «class»="equations">
-      </ul>
+          [equationsHtml]
-    </details>
+        </ul>
+      </details>
   else
-    return none
+    pure none
 
 def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   let equationsHtml ← equationsToHtml i
-  if let some equationsHtml ← equationsHtml then
+  if let some equationsHtml := equationsHtml then
-    #[equationsHtml]
+    pure #[equationsHtml]
   else
-    #[]
+    pure #[]
 
 end Output
 end DocGen4

DocGen4/Output/Index.lean

@@ -11,7 +11,7 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def index : HtmlM Html := do templateExtends (baseHtml "Index") $
+def index : HtmlM Html := do templateExtends (baseHtml "Index") $ pure $
   <main>
     <a id="top"></a>
     <h1> Welcome to the documentation page </h1>

DocGen4/Output/Inductive.lean

@@ -8,10 +8,10 @@ open scoped DocGen4.Jsx
 def ctorToHtml (i : NameInfo) : HtmlM Html := do
   let shortName := i.name.components'.head!.toString
   let name := i.name.toString
-  return <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
+  pure <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
-def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) :=
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
-  return #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
+  pure #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
 
 end Output
 end DocGen4

DocGen4/Output/Module.lean

@@ -31,9 +31,9 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   let inner := Html.element "span" true #[("class", "fn")] nodes
   let html := Html.element "span" false #[("class", "decl_args")] #[inner]
   if implicit then
-    <span «class»="impl_arg">{html}</span>
+    pure <span «class»="impl_arg">{html}</span>
   else
-    html
+    pure html
 
 def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
@@ -46,7 +46,7 @@ def structureInfoHeader (s : 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
-  nodes
+  pure nodes
 
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
@@ -69,7 +69,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
 
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
-  return <div «class»="decl_header"> [nodes] </div>
+  pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   let doc_html ← match doc with
@@ -79,18 +79,19 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   | DocInfo.definitionInfo i => definitionToHtml i
   | DocInfo.instanceInfo i => instanceToHtml i
   | DocInfo.classInductiveInfo i => classInductiveToHtml i
-  | _ => #[]
+  | _ => pure #[]
 
-  return <div «class»="decl" id={doc.getName.toString}>
+  pure
-    <div «class»={doc.getKind}>
+    <div «class»="decl" id={doc.getName.toString}>
-      <div «class»="gh_link">
+      <div «class»={doc.getKind}>
-        <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
+        <div «class»="gh_link">
+          <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
+        </div>
+        -- TODO: Attributes
+        {←docInfoHeader doc}
+        [doc_html]
       </div>
-      -- TODO: Attributes
-      {←docInfoHeader doc}
-      [←doc_html]
     </div>
-  </div>
 
 def declarationToNavLink (module : Name) : Html :=
   <div «class»="nav_link">
@@ -99,61 +100,62 @@ def declarationToNavLink (module : Name) : Html :=
 
 -- TODO: Similar functions are used all over the place, we should dedup them
 def moduleToNavLink (module : Name) : HtmlM Html := do
-  <a href={←moduleNameToLink module}>{module.toString}</a>
+  pure <a href={←moduleNameToLink module}>{module.toString}</a>
 
 def getImports (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+  let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
   let adj := res.importAdj.get! idx
   let mut imports := #[]
   for i in [:adj.size] do
     if adj.get! i then
       imports := imports.push (res.moduleNames.get! i)
-  imports
+  pure imports
 
 def getImportedBy (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+  let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
   let adj := res.importAdj
   let mut impBy := #[]
   for i in [:adj.size] do
     if adj.get! i |>.get! idx then
       impBy := impBy.push (res.moduleNames.get! i)
-  impBy
+  pure impBy
 
 def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
   let imports := (←getImportedBy moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do <li>{←moduleToNavLink i}</li>)
+  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
 
 
 def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
   let imports := (←getImports moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do <li>{←moduleToNavLink i}</li>)
+  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
 
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
-  <nav «class»="internal_nav">
+  pure
-    <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
+    <nav «class»="internal_nav">
-    <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
+      <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-    <div «class»="imports">
+      <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
-      <details>
+      <div «class»="imports">
-        <summary>Imports</summary>
+        <details>
-        <ul>
+          <summary>Imports</summary>
-          [←importsHtml moduleName]
+          <ul>
-        </ul>
+            [←importsHtml moduleName]
-      </details>
+          </ul>
-      <details>
+        </details>
-        <summary>Imported by</summary>
+        <details>
-        <ul>
+          <summary>Imported by</summary>
-          [←importedByHtml moduleName]
+          <ul>
-        </ul>
+            [←importedByHtml moduleName]
-      </details>
+          </ul>
-    </div>
+        </details>
-    [members.map declarationToNavLink]
+      </div>
-  </nav>
+      [members.map declarationToNavLink]
+    </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
   let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
-  templateExtends (baseHtmlArray module.name.toString) $ #[
+  templateExtends (baseHtmlArray module.name.toString) $ pure #[
     ←internalNav (module.members.map DocInfo.getName) module.name,
     Html.element "main" false #[] docInfos
   ]

DocGen4/Output/Navbar.lean

@@ -13,8 +13,8 @@ namespace Output
 open Lean
 open scoped DocGen4.Jsx
 
-def moduleListFile (file : Name) : HtmlM Html :=
+def moduleListFile (file : Name) : HtmlM Html := do
-  return <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+  pure <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>
 
@@ -25,36 +25,38 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let dirNodes ← (dirs.mapM moduleListDir)
   let fileNodes ← (files.mapM moduleListFile)
   let moduleLink ← moduleNameToLink h.getName
-  return <details "class"="nav_sect" "data-path"={moduleLink}
+  pure
-      [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
+    <details "class"="nav_sect" "data-path"={moduleLink}
-    <summary>{h.getName.toString}</summary>
+      [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
-    [dirNodes]
+      <summary>{h.getName.toString}</summary>
-    [fileNodes]
+      [dirNodes]
-  </details>
+      [fileNodes]
+    </details>
 
 def moduleList : HtmlM Html := do
   let hierarchy := (←getResult).hierarchy
   let mut list := Array.empty
   for (n, cs) in hierarchy.getChildren do
     list := list.push $ ←moduleListDir cs
-  return <div "class"="module_list">[list]</div>
+  pure <div "class"="module_list">[list]</div>
 
 def navbar : HtmlM Html := do
-  <nav «class»="nav">
+  pure
-    <h3>General documentation</h3>
+    <nav «class»="nav">
-    <div «class»="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
+      <h3>General documentation</h3>
-    /-
+      <div «class»="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
-    TODO: Add these in later
+      /-
-    <div «class»="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
+      TODO: Add these in later
-    <div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
+      <div «class»="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
-    <div «class»="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
+      <div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
-    <div «class»="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
+      <div «class»="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
-    <div «class»="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
+      <div «class»="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
-    <div «class»="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
+      <div «class»="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
-    -/
+      <div «class»="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
-    <h3>Library</h3>
+      -/
-    {← moduleList}
+      <h3>Library</h3>
-  </nav>
+      {← moduleList}
+    </nav>
 
 end Output
 end DocGen4

DocGen4/Output/NotFound.lean

@@ -11,7 +11,7 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def notFound : HtmlM Html := do templateExtends (baseHtml "404") $
+def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ pure $
   <main>
     <h1>404 Not Found</h1>
     <p> Unfortunately, the page you were looking for is no longer here. </p>

DocGen4/Output/Structure.lean

@@ -9,16 +9,18 @@ open Lean
 def fieldToHtml (f : NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
-  return <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
+  pure <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
   if Name.isSuffixOf `mk i.ctor.name then
-    #[<ul «class»="structure_fields" id={i.ctor.name.toString}>
+    pure #[
-      [←i.fieldInfo.mapM fieldToHtml]
+      <ul «class»="structure_fields" id={i.ctor.name.toString}>
-    </ul>]
+        [←i.fieldInfo.mapM fieldToHtml]
+      </ul>]
   else
     let ctorShortName := i.ctor.name.components'.head!.toString
-    #[<ul «class»="structure_ext">
+    pure #[
+      <ul «class»="structure_ext">
         <li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
         <ul «class»="structure_ext_fields">
           [←i.fieldInfo.mapM fieldToHtml]

DocGen4/Output/Template.lean

@@ -12,44 +12,45 @@ namespace Output
 open scoped DocGen4.Jsx
 
 def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
-  <html lang="en">
+  pure
-    <head>
+    <html lang="en">
-      <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
+      <head>
-      <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
+        <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
-      <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
+        <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
-      <title>{title}</title>
+        <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
-      <meta charset="UTF-8"/>
+        <title>{title}</title>
-      <meta name="viewport" content="width=device-width, initial-scale=1"/>
+        <meta charset="UTF-8"/>
-    </head>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
-    
+      </head>
-    <body>
+      
+      <body>
 
-    <input id="nav_toggle" type="checkbox"/>
+      <input id="nav_toggle" type="checkbox"/>
 
-    <header>
+      <header>
-      <h1><label «for»="nav_toggle"></label>Documentation</h1>
+        <h1><label «for»="nav_toggle"></label>Documentation</h1>
-      <p «class»="header_filename break_within">{title}</p>
+        <p «class»="header_filename break_within">{title}</p>
-      -- TODO: Replace this form with our own search
+        -- TODO: Replace this form with our own search
-      <form action="https://google.com/search" method="get" id="search_form">
+        <form action="https://google.com/search" method="get" id="search_form">
-        <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
+          <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
-        <input type="text" name="q" autocomplete="off"/>
+          <input type="text" name="q" autocomplete="off"/>
-        <button>Google site search</button>
+          <button>Google site search</button>
-      </form>
+        </form>
-    </header>
+      </header>
 
-    [site]
+      [site]
-    
+      
-    {←navbar}
+      {←navbar}
 
-    -- Lean in JS in HTML in Lean...very meta
+      -- Lean in JS in HTML in Lean...very meta
-    <script>
+      <script>
-      siteRoot = "{←getRoot}";
+        siteRoot = "{←getRoot}";
-    </script>
+      </script>
 
-    -- TODO Add more js stuff
+      -- TODO Add more js stuff
-    <script src={s!"{←getRoot}nav.js"}></script>
+      <script src={s!"{←getRoot}nav.js"}></script>
-    </body>
+      </body>
-  </html>
+    </html>
 
 
 def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site]

DocGen4/Process.lean

@@ -140,7 +140,7 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
     openDecls := ← getOpenDecls
     fileMap := default
   }
-  return tagExprInfos ctx infos tt
+  pure $ tagExprInfos ctx infos tt
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
@@ -150,16 +150,16 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let doc ← findDocString? env v.name
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
-  | some range => return Info.mk ⟨v.name, type⟩ args doc range.range
+  | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range
   | none => panic! s!"{v.name} is a declaration without position"
 
 def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  return AxiomInfo.mk info v.isUnsafe
+  pure $ AxiomInfo.mk info v.isUnsafe
 
 def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  return TheoremInfo.mk info
+  pure $ TheoremInfo.mk info
 
 def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -167,13 +167,13 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
   let env ← getEnv
   let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
   if isPartial then
-    return OpaqueInfo.mk info t DefinitionSafety.partial
+    pure $ OpaqueInfo.mk info t DefinitionSafety.partial
   else
     let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
-    return OpaqueInfo.mk info t safety
+    pure $ OpaqueInfo.mk info t safety
 
 def isInstance (declName : Name) : MetaM Bool := do
-  return (instanceExtension.getState (←getEnv)).instanceNames.contains declName
+  pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName
 
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
@@ -213,7 +213,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
       pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq])
   catch err =>
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
-    return DefinitionInfo.mk info isUnsafe v.hints none
+    pure $ DefinitionInfo.mk info isUnsafe v.hints none
 
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
@@ -225,7 +225,7 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
   let ctors ← v.ctors.mapM (λ name => do pure $ NameInfo.mk name (←getConstructorType name))
-  return InductiveInfo.mk info ctors v.isUnsafe
+  pure $ InductiveInfo.mk info ctors v.isUnsafe
 
 def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
   match type, n with
@@ -243,7 +243,7 @@ def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : Meta
   let mut field_infos := #[]
   for (name, type) in fields do
     field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
-  return field_infos
+  pure $ field_infos
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -254,24 +254,24 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   match getStructureInfo? env v.name with
   | some i =>
     if i.fieldNames.size - parents.size > 0 then
-      return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
     else
-      return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
   | none => panic! s!"{v.name} is not a structure"
 
 def getInstances (className : Name) : MetaM (Array Name) := do
   let fn ← mkConstWithFreshMVarLevels className
   let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
   let insts ← SynthInstance.getInstances (mkAppN fn xs)
-  return insts.map Expr.constName!
+  pure $ insts.map Expr.constName!
 
 def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
   let sinfo ← StructureInfo.ofInductiveVal v
-  return ClassInfo.mk sinfo (←getInstances v.name)
+  pure $ ClassInfo.mk sinfo (←getInstances v.name)
 
 def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
   let info ← InductiveInfo.ofInductiveVal v
-  return ClassInductiveInfo.mk info (←getInstances v.name)
+  pure $ ClassInductiveInfo.mk info (←getInstances v.name)
 
 namespace DocInfo
 
@@ -290,18 +290,18 @@ def isBlackListed (declName : Name) : MetaM Bool := do
 -- TODO: Is this actually the best way?
 def isProjFn (declName : Name) : MetaM Bool := do
   let env ← getEnv
-  return match declName with
+  match declName with
   | Name.str parent name _ =>
     if isStructure env parent then
       match getStructureInfo? env parent with
       | some i =>
         match i.fieldNames.find? (· == name) with
-        | some _ => true
+        | some _ => pure true
-        | none => false
+        | none => pure false
       | none => panic! s!"{parent} is not a structure"
     else
-      false
+      pure false
-  | _ => false
+  | _ => pure false
 
 def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
   if (←isBlackListed name) then
@@ -446,7 +446,7 @@ def process : MetaM AnalyzerResult := do
       let some importIdx := env.getModuleIdx? imp.module | unreachable!
       adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
 
-  return {
+  pure {
     name2ModIdx := env.const2ModIdx,
     moduleNames := env.header.moduleNames,
     moduleInfo := res,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-08
+leanprover/lean4:nightly-2022-02-11