From c2d18fe3b156edc647dea3533edfee06b3fe02e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 6 Feb 2022 17:06:22 +0100
Subject: [PATCH 1/7] feat: tag declarations with unsafe and partial

---
 DocGen4/Output/Module.lean |  6 +-----
 DocGen4/Process.lean       | 43 +++++++++++++++++++++++++++++---------
 2 files changed, 34 insertions(+), 15 deletions(-)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index d203241..81a3db7 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -49,9 +49,7 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
 
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
-  -- TODO: noncomputable, partial
-  -- TODO: Support all the kinds in CSS
-  nodes := nodes.push <span «class»="decl_kind">{doc.getKind}</span>
+  nodes := nodes.push <span «class»="decl_kind">{doc.getKindDescription}</span>
   nodes := nodes.push
     <span «class»="decl_name">
       <a «class»="break_within" href={←declNameToLink doc.getName}>
@@ -84,7 +82,6 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   return <div «class»="decl" id={doc.getName.toString}>
     <div «class»={doc.getKind}>
       <div «class»="gh_link">
-        -- TODO: Put the proper source link
         <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
       </div>
       -- TODO: Attributes
@@ -134,7 +131,6 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
   <nav «class»="internal_nav">
     <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-    -- TODO: Proper source links
     <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
     <div «class»="imports">
       <details>
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 5a5df9e..5a93c33 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -40,12 +40,14 @@ structure TheoremInfo extends Info
 
 structure OpaqueInfo extends Info where
   value : CodeWithInfos
-  isUnsafe : Bool
+  -- A value of partial is interpreted as this constant being part of a partial def
+  -- since the actual definition for a partial def is hidden behind an inaccessible value
+  unsafeInformation : DefinitionSafety
   deriving Inhabited
 
 structure DefinitionInfo extends Info where
-  --value : CodeWithInfos
-  unsafeInformation : DefinitionSafety
+  -- partial defs are handled by OpaqueInfo
+  isUnsafe : Bool
   hints : ReducibilityHints
   equations : Option (Array CodeWithInfos)
   deriving Inhabited
@@ -156,12 +158,17 @@ def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
 def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let t ← prettyPrintTerm v.value
-  return OpaqueInfo.mk info t v.isUnsafe
+  let env ← getEnv
+  let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
+  if isPartial then
+    return OpaqueInfo.mk info t DefinitionSafety.partial
+  else
+    let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+    return OpaqueInfo.mk info t safety
 
 def isInstance (declName : Name) : MetaM Bool := do
   (instanceExtension.getState (←getEnv)).instanceNames.contains declName
 
-
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
   | Expr.lam name type body data =>
@@ -188,18 +195,19 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
 
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
+  let isUnsafe := v.safety == DefinitionSafety.unsafe
   try
     let eqs? ← getEqnsFor? v.name
     match eqs? with
     | some eqs =>
       let prettyEqs ← eqs.mapM processEq
-      DefinitionInfo.mk info v.safety v.hints prettyEqs
+      DefinitionInfo.mk info isUnsafe v.hints prettyEqs
     | none =>
       let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
-      DefinitionInfo.mk info v.safety v.hints (some #[eq])
+      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 v.safety v.hints none
+    return DefinitionInfo.mk info isUnsafe v.hints none
 
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
@@ -327,10 +335,25 @@ def getKind : DocInfo → String
 | theoremInfo _ => "theorem"
 | opaqueInfo _ => "constant"
 | definitionInfo _ => "def"
-| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
+| instanceInfo _ => "instance"
 | inductiveInfo _ => "inductive"
 | structureInfo _ => "structure"
-| classInfo _ => "class" -- TODO: This is handled as structure right now
+| classInfo _ => "class"
+
+open DefinitionSafety in
+def getKindDescription : DocInfo → String
+| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo i =>
+  match i.unsafeInformation with
+  | safe => "constant"
+  | «unsafe» => "unsafe constant"
+  | «partial» => "partial def"
+| definitionInfo i => if i.isUnsafe then "unsafe def" else "def"
+| instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance"
+| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
 
 def getType : DocInfo → CodeWithInfos
 | axiomInfo i => i.type

From 27f8b5076350c4b191c43215adeb9fac3f25ebd6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 6 Feb 2022 17:28:56 +0100
Subject: [PATCH 2/7] feat: tag abbrevs

---
 DocGen4/Process.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 5a93c33..c38559f 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -340,16 +340,21 @@ def getKind : DocInfo → String
 | structureInfo _ => "structure"
 | classInfo _ => "class"
 
-open DefinitionSafety in
 def getKindDescription : DocInfo → String
 | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
 | theoremInfo _ => "theorem"
 | opaqueInfo i =>
   match i.unsafeInformation with
-  | safe => "constant"
-  | «unsafe» => "unsafe constant"
-  | «partial» => "partial def"
-| definitionInfo i => if i.isUnsafe then "unsafe def" else "def"
+  | DefinitionSafety.safe => "constant"
+  | DefinitionSafety.unsafe => "unsafe constant"
+  | DefinitionSafety.partial => "partial def"
+| definitionInfo i =>
+  if i.hints.isAbbrev then
+    "abbrev"
+  else if i.isUnsafe then
+    "unsafe def"
+  else
+    "def"
 | instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance"
 | inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
 | structureInfo _ => "structure"

From 8059940c309ffd8dc4102f5bbddde2b48dbccc2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 6 Feb 2022 20:14:36 +0100
Subject: [PATCH 3/7] feat: class inductives

---
 DocGen4/Output/Class.lean          |  6 +++---
 DocGen4/Output/ClassInductive.lean | 13 +++++++++++++
 DocGen4/Output/Module.lean         |  2 ++
 DocGen4/Process.lean               | 31 +++++++++++++++++++++++++-----
 4 files changed, 44 insertions(+), 8 deletions(-)
 create mode 100644 DocGen4/Output/ClassInductive.lean

diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
index f803a6d..e7eb3c1 100644
--- a/DocGen4/Output/Class.lean
+++ b/DocGen4/Output/Class.lean
@@ -10,8 +10,8 @@ open Lean
 def classInstanceToHtml (name : Name) : HtmlM Html := do
   <li><a href={←declNameToLink name}>{name.toString}</a></li>
 
-def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
-  let instancesHtml ← i.instances.mapM classInstanceToHtml
+def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
+  let instancesHtml ← instances.mapM classInstanceToHtml
   return <details «class»="instances">
         <summary>Instances</summary>
         <ul>
@@ -20,7 +20,7 @@ def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
     </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i)
+  (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
new file mode 100644
index 0000000..0e07f72
--- /dev/null
+++ b/DocGen4/Output/ClassInductive.lean
@@ -0,0 +1,13 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Class
+import DocGen4.Output.Inductive
+
+
+namespace DocGen4
+namespace Output
+
+def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
+  (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 81a3db7..6e50374 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -9,6 +9,7 @@ import DocGen4.Output.Structure
 import DocGen4.Output.Class
 import DocGen4.Output.Definition
 import DocGen4.Output.Instance
+import DocGen4.Output.ClassInductive
 
 namespace DocGen4
 namespace Output
@@ -77,6 +78,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   | DocInfo.classInfo i => classToHtml i
   | DocInfo.definitionInfo i => definitionToHtml i
   | DocInfo.instanceInfo i => instanceToHtml i
+  | DocInfo.classInductiveInfo i => classInductiveToHtml i
   | _ => #[]
 
   return <div «class»="decl" id={doc.getName.toString}>
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index c38559f..34ea5e7 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -69,6 +69,10 @@ structure ClassInfo extends StructureInfo where
   instances : Array Name
   deriving Inhabited
 
+structure ClassInductiveInfo extends InductiveInfo where
+  instances : Array Name
+  deriving Inhabited
+
 inductive DocInfo where
 | axiomInfo (info : AxiomInfo) : DocInfo
 | theoremInfo (info : TheoremInfo) : DocInfo
@@ -78,6 +82,7 @@ inductive DocInfo where
 | inductiveInfo (info : InductiveInfo) : DocInfo
 | structureInfo (info : StructureInfo) : DocInfo
 | classInfo (info : ClassInfo) : DocInfo
+| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
   deriving Inhabited
 
 namespace DocInfo
@@ -91,6 +96,7 @@ def getDeclarationRange : DocInfo → DeclarationRange
 | inductiveInfo i => i.declarationRange
 | structureInfo i => i.declarationRange
 | classInfo i => i.declarationRange
+| classInductiveInfo i => i.declarationRange
 
 def lineOrder (l r : DocInfo) : Bool :=
   l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
@@ -253,12 +259,19 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
       return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
   | none => panic! s!"{v.name} is not a structure"
 
-def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
-  let sinfo ← StructureInfo.ofInductiveVal v
-  let fn ← mkConstWithFreshMVarLevels v.name
+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 ClassInfo.mk sinfo (insts.map Expr.constName!)
+  insts.map Expr.constName!
+
+def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
+  let sinfo ← StructureInfo.ofInductiveVal v
+  return 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)
 
 namespace DocInfo
 
@@ -314,7 +327,10 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
       else
         some $ structureInfo (←StructureInfo.ofInductiveVal i)
     else
-      some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
+      if isClass env i.name then
+        some $ classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
+      else
+        some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
   -- we ignore these for now
   | ConstantInfo.ctorInfo i => none
   | ConstantInfo.recInfo i => none
@@ -329,6 +345,7 @@ def getName : DocInfo → Name
 | inductiveInfo i => i.name
 | structureInfo i => i.name
 | classInfo i => i.name
+| classInductiveInfo i => i.name
 
 def getKind : DocInfo → String
 | axiomInfo _ => "axiom"
@@ -339,6 +356,7 @@ def getKind : DocInfo → String
 | inductiveInfo _ => "inductive"
 | structureInfo _ => "structure"
 | classInfo _ => "class"
+| classInductiveInfo _ => "class"
 
 def getKindDescription : DocInfo → String
 | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
@@ -359,6 +377,7 @@ def getKindDescription : DocInfo → String
 | inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
 | structureInfo _ => "structure"
 | classInfo _ => "class"
+| classInductiveInfo _ => "class inductive"
 
 def getType : DocInfo → CodeWithInfos
 | axiomInfo i => i.type
@@ -369,6 +388,7 @@ def getType : DocInfo → CodeWithInfos
 | inductiveInfo i => i.type
 | structureInfo i => i.type
 | classInfo i => i.type
+| classInductiveInfo i => i.type
 
 def getArgs : DocInfo → Array Arg
 | axiomInfo i => i.args
@@ -379,6 +399,7 @@ def getArgs : DocInfo → Array Arg
 | inductiveInfo i => i.args
 | structureInfo i => i.args
 | classInfo i => i.args
+| classInductiveInfo i => i.args
 
 end DocInfo
 

From 00bf10c6f0f89b19b1c7feab74984ba81b2c6d2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 9 Feb 2022 22:45:28 +0100
Subject: [PATCH 4/7] chore: bump toolchain

---
 DocGen4/Process.lean      | 62 +++++++++++++++++++--------------------
 DocGen4/ToHtmlFormat.lean |  8 ++---
 lean-toolchain            |  2 +-
 3 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 34ea5e7..c4b0e46 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -140,13 +140,13 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
     openDecls := ← getOpenDecls
     fileMap := default
   }
-  tagExprInfos ctx infos tt
+  return tagExprInfos ctx infos tt
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
   let (args, type) := typeToArgsType v.type
   let type ← prettyPrintTerm type
-  let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b)
+  let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
   let doc ← findDocString? env v.name
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
@@ -173,7 +173,7 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
     return OpaqueInfo.mk info t safety
 
 def isInstance (declName : Name) : MetaM Bool := do
-  (instanceExtension.getState (←getEnv)).instanceNames.contains declName
+  return (instanceExtension.getState (←getEnv)).instanceNames.contains declName
 
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
@@ -197,7 +197,7 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
       let us := v.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
       let type ← mkForallFVars xs type
-      type
+      pure type
 
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -207,10 +207,10 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
     match eqs? with
     | some eqs =>
       let prettyEqs ← eqs.mapM processEq
-      DefinitionInfo.mk info isUnsafe v.hints prettyEqs
+      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs
     | none =>
       let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
-      DefinitionInfo.mk info isUnsafe v.hints (some #[eq])
+      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
@@ -218,13 +218,13 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
   match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type
+  | some (ConstantInfo.ctorInfo i) => prettyPrintTerm i.type
   | _ => panic! s!"Constructor {ctor} was requested but does not exist"
 
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
+  let ctors ← v.ctors.mapM (λ name => do pure $ NameInfo.mk name (←getConstructorType name))
   return InductiveInfo.mk info ctors v.isUnsafe
 
 def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
@@ -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}
-  field_infos
+  return field_infos
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -263,7 +263,7 @@ def getInstances (className : Name) : MetaM (Array Name) := do
   let fn ← mkConstWithFreshMVarLevels className
   let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
   let insts ← SynthInstance.getInstances (mkAppN fn xs)
-  insts.map Expr.constName!
+  return insts.map Expr.constName!
 
 def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
   let sinfo ← StructureInfo.ofInductiveVal v
@@ -279,18 +279,18 @@ def isBlackListed (declName : Name) : MetaM Bool := do
   match ←findDeclarationRanges? declName with
   | some _ =>
     let env ← getEnv
-    declName.isInternal
-    <||> isAuxRecursor env declName
-    <||> isNoConfusion env declName
+    pure (declName.isInternal)
+    <||> (pure $ isAuxRecursor env declName)
+    <||> (pure $ isNoConfusion env declName)
     <||> isRec declName
     <||> isMatcher declName
   -- TODO: Evaluate whether filtering out declarations without range is sensible
-  | none => true
+  | none => pure true
 
 -- TODO: Is this actually the best way?
 def isProjFn (declName : Name) : MetaM Bool := do
   let env ← getEnv
-  match declName with
+  return match declName with
   | Name.str parent name _ =>
     if isStructure env parent then
       match getStructureInfo? env parent with
@@ -307,34 +307,34 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
   if (←isBlackListed name) then
     return none
   match info with
-  | ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i)
-  | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i)
-  | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
+  | ConstantInfo.axiomInfo i => pure <| some <| axiomInfo (←AxiomInfo.ofAxiomVal i)
+  | ConstantInfo.thmInfo i => pure <| some <| theoremInfo (←TheoremInfo.ofTheoremVal i)
+  | ConstantInfo.opaqueInfo i => pure <| some <| opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
   | ConstantInfo.defnInfo i =>
     if ← (isProjFn i.name) then
-      none
+      pure none
     else
       let info ← DefinitionInfo.ofDefinitionVal i
       if (←isInstance i.name) then
-        some $ instanceInfo info
+        pure <| some <| instanceInfo info
       else
-        some $ definitionInfo info
+        pure <| some <| definitionInfo info
   | ConstantInfo.inductInfo i =>
     let env ← getEnv
     if isStructure env i.name then
       if isClass env i.name then
-        some $ classInfo (←ClassInfo.ofInductiveVal i)
+        pure <| some <| classInfo (←ClassInfo.ofInductiveVal i)
       else
-        some $ structureInfo (←StructureInfo.ofInductiveVal i)
+        pure <| some <| structureInfo (←StructureInfo.ofInductiveVal i)
     else
       if isClass env i.name then
-        some $ classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
+        pure <| some <| classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
       else
-        some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
+        pure <| some <| inductiveInfo (←InductiveInfo.ofInductiveVal i)
   -- we ignore these for now
-  | ConstantInfo.ctorInfo i => none
-  | ConstantInfo.recInfo i => none
-  | ConstantInfo.quotInfo i => none
+  | ConstantInfo.ctorInfo i => pure none
+  | ConstantInfo.recInfo i => pure none
+  | ConstantInfo.quotInfo i => pure none
 
 def getName : DocInfo → Name
 | axiomInfo i => i.name
@@ -428,7 +428,7 @@ def process : MetaM AnalyzerResult := do
     try
       let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
       if let some dinfo ← analysis then
-        let some modidx ← env.getModuleIdxFor? dinfo.getName | unreachable!
+        let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable!
         let moduleName := env.allImportedModuleNames.get! modidx
         let module := res.find! moduleName
         res := res.insert moduleName {module with members := module.members.push dinfo}
@@ -440,10 +440,10 @@ def process : MetaM AnalyzerResult := do
   -- TODO: This could probably be faster if we did an insertion sort above instead
   for (moduleName, module) in res.toArray do
     res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
-    let some modIdx ← env.getModuleIdx? moduleName | unreachable!
+    let some modIdx := env.getModuleIdx? moduleName | unreachable!
     let moduleData := env.header.moduleData.get! modIdx
     for imp in moduleData.imports do
-      let some importIdx ← env.getModuleIdx? imp.module | unreachable!
+      let some importIdx := env.getModuleIdx? imp.module | unreachable!
       adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
 
   return {
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index 253de07..beddf74 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -86,12 +86,12 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
     as ← match attr with
     | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
       let n ← match n with
-        | `(jsxAttrName| $n:strLit) => n
-        | `(jsxAttrName| $n:ident) => quote (toString n.getId)
+        | `(jsxAttrName| $n:strLit) => pure n
+        | `(jsxAttrName| $n:ident) => pure $ quote (toString n.getId)
         | _ => Macro.throwUnsupported
       let v ← match v with
-        | `(jsxAttrVal| {$v}) => v
-        | `(jsxAttrVal| $v:strLit) => v
+        | `(jsxAttrVal| {$v}) => pure v
+        | `(jsxAttrVal| $v:strLit) => pure v
         | _ => Macro.throwUnsupported
       `(($as).push ($n, ($v : String)))
     | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
diff --git a/lean-toolchain b/lean-toolchain
index 1de6590..a68e3bc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-04
\ No newline at end of file
+leanprover/lean4:nightly-2022-02-08
\ No newline at end of file

From d39b14cf7a804b8f1ef36bc230f448fdea397026 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 12 Feb 2022 15:09:13 +0100
Subject: [PATCH 5/7] chore: bump toolchain, bye auto pure

---
 DocGen4/IncludeStr.lean            |  2 +-
 DocGen4/Load.lean                  |  4 +-
 DocGen4/Output.lean                | 10 ++--
 DocGen4/Output/Base.lean           | 24 ++++-----
 DocGen4/Output/Class.lean          |  7 +--
 DocGen4/Output/ClassInductive.lean |  2 +-
 DocGen4/Output/Definition.lean     | 25 ++++-----
 DocGen4/Output/Index.lean          |  2 +-
 DocGen4/Output/Inductive.lean      |  6 +--
 DocGen4/Output/Module.lean         | 82 +++++++++++++++---------------
 DocGen4/Output/Navbar.lean         | 50 +++++++++---------
 DocGen4/Output/NotFound.lean       |  2 +-
 DocGen4/Output/Structure.lean      | 12 +++--
 DocGen4/Output/Template.lean       | 67 ++++++++++++------------
 DocGen4/Process.lean               | 42 +++++++--------
 lean-toolchain                     |  2 +-
 16 files changed, 174 insertions(+), 165 deletions(-)

diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean
index 6946ab5..511a181 100644
--- a/DocGen4/IncludeStr.lean
+++ b/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"
 
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 5f23a57..20da38a 100644
--- a/DocGen4/Load.lean
+++ b/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
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index eacb9e7..85b90f4 100644
--- a/DocGen4/Output.lean
+++ b/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
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 48e86ad..f66a37e 100644
--- a/DocGen4/Output/Base.lean
+++ b/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 getResult : HtmlM AnalyzerResult := do (←read).result
-def getCurrentName : HtmlM (Option Name) := do (←read).currentName
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do (←read).sourceLinker module range
+def getRoot : HtmlM String := do pure (←read).root
+def getResult : HtmlM AnalyzerResult := do pure (←read).result
+def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
+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.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[]
+  | TaggedText.text t => pure #[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)]
-    | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+         pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+    | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
index e7eb3c1..7f64cc0 100644
--- a/DocGen4/Output/Class.lean
+++ b/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
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
index 0e07f72..6113e73 100644
--- a/DocGen4/Output/ClassInductive.lean
+++ b/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
diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index f92627c..64813d4 100644
--- a/DocGen4/Output/Definition.lean
+++ b/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>
-      <summary>Equations</summary>
-      <ul «class»="equations">
-        [equationsHtml]
-      </ul>
-    </details>
+    pure
+      <details>
+        <summary>Equations</summary>
+        <ul «class»="equations">
+          [equationsHtml]
+        </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
-    #[equationsHtml]
+  if let some equationsHtml := equationsHtml then
+    pure #[equationsHtml]
   else
-    #[]
+    pure #[]
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index b09ac47..e0342b6 100644
--- a/DocGen4/Output/Index.lean
+++ b/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>
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 0aa9444..d8f84df 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/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) :=
-  return #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
+  pure #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 6e50374..94d7827 100644
--- a/DocGen4/Output/Module.lean
+++ b/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}>
-    <div «class»={doc.getKind}>
-      <div «class»="gh_link">
-        <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
+  pure
+    <div «class»="decl" id={doc.getName.toString}>
+      <div «class»={doc.getKind}>
+        <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">
-    <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-    <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
-    <div «class»="imports">
-      <details>
-        <summary>Imports</summary>
-        <ul>
-          [←importsHtml moduleName]
-        </ul>
-      </details>
-      <details>
-        <summary>Imported by</summary>
-        <ul>
-          [←importedByHtml moduleName]
-        </ul>
-      </details>
-    </div>
-    [members.map declarationToNavLink]
-  </nav>
+  pure
+    <nav «class»="internal_nav">
+      <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
+      <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
+      <div «class»="imports">
+        <details>
+          <summary>Imports</summary>
+          <ul>
+            [←importsHtml moduleName]
+          </ul>
+        </details>
+        <details>
+          <summary>Imported by</summary>
+          <ul>
+            [←importedByHtml moduleName]
+          </ul>
+        </details>
+      </div>
+      [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
   ]
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index fee4598..d2d4792 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -13,8 +13,8 @@ namespace Output
 open Lean
 open scoped DocGen4.Jsx
 
-def moduleListFile (file : Name) : HtmlM Html :=
-  return <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+def moduleListFile (file : Name) : HtmlM Html := do
+  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}
-      [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
-    <summary>{h.getName.toString}</summary>
-    [dirNodes]
-    [fileNodes]
-  </details>
+  pure
+    <details "class"="nav_sect" "data-path"={moduleLink}
+      [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
+      <summary>{h.getName.toString}</summary>
+      [dirNodes]
+      [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">
-    <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>
-    <div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</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}attributes.html"}>attributes</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}
-  </nav>
+  pure
+    <nav «class»="nav">
+      <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>
+      <div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</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}attributes.html"}>attributes</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}
+    </nav>
 
 end Output
 end DocGen4
diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean
index ed5d547..a700963 100644
--- a/DocGen4/Output/NotFound.lean
+++ b/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>
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index 688324f..23212ae 100644
--- a/DocGen4/Output/Structure.lean
+++ b/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}>
-      [←i.fieldInfo.mapM fieldToHtml]
-    </ul>]
+    pure #[
+      <ul «class»="structure_fields" id={i.ctor.name.toString}>
+        [←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]
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index a22e9d6..72727a8 100644
--- a/DocGen4/Output/Template.lean
+++ b/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">
-    <head>
-      <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
-      <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
-      <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
-      <title>{title}</title>
-      <meta charset="UTF-8"/>
-      <meta name="viewport" content="width=device-width, initial-scale=1"/>
-    </head>
-    
-    <body>
+  pure
+    <html lang="en">
+      <head>
+        <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
+        <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
+        <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
+        <title>{title}</title>
+        <meta charset="UTF-8"/>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+      </head>
+      
+      <body>
 
-    <input id="nav_toggle" type="checkbox"/>
+      <input id="nav_toggle" type="checkbox"/>
 
-    <header>
-      <h1><label «for»="nav_toggle"></label>Documentation</h1>
-      <p «class»="header_filename break_within">{title}</p>
-      -- TODO: Replace this form with our own search
-      <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="text" name="q" autocomplete="off"/>
-        <button>Google site search</button>
-      </form>
-    </header>
+      <header>
+        <h1><label «for»="nav_toggle"></label>Documentation</h1>
+        <p «class»="header_filename break_within">{title}</p>
+        -- TODO: Replace this form with our own search
+        <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="text" name="q" autocomplete="off"/>
+          <button>Google site search</button>
+        </form>
+      </header>
 
-    [site]
-    
-    {←navbar}
+      [site]
+      
+      {←navbar}
 
-    -- Lean in JS in HTML in Lean...very meta
-    <script>
-      siteRoot = "{←getRoot}";
-    </script>
+      -- Lean in JS in HTML in Lean...very meta
+      <script>
+        siteRoot = "{←getRoot}";
+      </script>
 
-    -- TODO Add more js stuff
-    <script src={s!"{←getRoot}nav.js"}></script>
-    </body>
-  </html>
+      -- TODO Add more js stuff
+      <script src={s!"{←getRoot}nav.js"}></script>
+      </body>
+    </html>
 
 
 def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site]
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index c4b0e46..363863d 100644
--- a/DocGen4/Process.lean
+++ b/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
-        | none => false
+        | some _ => pure true
+        | none => pure false
       | none => panic! s!"{parent} is not a structure"
     else
-      false
-  | _ => false
+      pure 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,
diff --git a/lean-toolchain b/lean-toolchain
index a68e3bc..4b598af 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-08
\ No newline at end of file
+leanprover/lean4:nightly-2022-02-11

From 59e50943d61023279266ba6231694cbcff5032d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 12 Feb 2022 15:57:45 +0100
Subject: [PATCH 6/7] feat: mark noncomputable defs and instances

---
 DocGen4/Process.lean | 39 ++++++++++++++++++++++++++++++---------
 1 file changed, 30 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 363863d..cb3df71 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -50,6 +50,7 @@ structure DefinitionInfo extends Info where
   isUnsafe : Bool
   hints : ReducibilityHints
   equations : Option (Array CodeWithInfos)
+  isComputable : Bool
   deriving Inhabited
 
 abbrev InstanceInfo := DefinitionInfo
@@ -199,21 +200,28 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
       let type ← mkForallFVars xs type
       pure type
 
+-- The following code is translated from ll_infer_type.cpp
+def computable? (defn : Name) : MetaM Bool := do
+  let cstage2Name := defn.append `_cstage2
+  let env ← getEnv
+  pure $ env.find? cstage2Name |>.isSome
+
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let isUnsafe := v.safety == DefinitionSafety.unsafe
+  let isComputable ← computable? v.name
   try
     let eqs? ← getEqnsFor? v.name
     match eqs? with
     | some eqs =>
       let prettyEqs ← eqs.mapM processEq
-      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs
+      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isComputable
     | none =>
       let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
-      pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq])
+      pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isComputable
   catch err =>
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
-    pure $ DefinitionInfo.mk info isUnsafe v.hints none
+    pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable
 
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
@@ -366,14 +374,27 @@ def getKindDescription : DocInfo → String
   | DefinitionSafety.safe => "constant"
   | DefinitionSafety.unsafe => "unsafe constant"
   | DefinitionSafety.partial => "partial def"
-| definitionInfo i =>
+| definitionInfo i => Id.run do
   if i.hints.isAbbrev then
-    "abbrev"
-  else if i.isUnsafe then
-    "unsafe def"
+    pure "abbrev"
   else
-    "def"
-| instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance"
+    let mut modifiers := #[]
+    if i.isUnsafe then
+      modifiers := modifiers.push "unsafe"
+    if ¬i.isComputable then
+      modifiers := modifiers.push "noncomputable"
+
+    modifiers := modifiers.push "def"
+    pure $ String.intercalate " " modifiers.toList
+| instanceInfo i => Id.run do
+  let mut modifiers := #[]
+  if i.isUnsafe then
+    modifiers := modifiers.push "unsafe"
+  if ¬i.isComputable then
+    modifiers := modifiers.push "noncomputable"
+
+  modifiers := modifiers.push "instance"
+  pure $ String.intercalate " " modifiers.toList
 | inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
 | structureInfo _ => "structure"
 | classInfo _ => "class"

From d700da7284c8d9561d5dd76493d2641cbbe8bbbb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 13 Feb 2022 03:32:53 +0100
Subject: [PATCH 7/7] feat: Attributes

---
 DocGen4.lean               |   1 +
 DocGen4/Attributes.lean    | 110 +++++++++++++++++++++++++++++++++++++
 DocGen4/Output/Module.lean |  14 ++++-
 DocGen4/Process.lean       |  30 ++++++++--
 4 files changed, 147 insertions(+), 8 deletions(-)
 create mode 100644 DocGen4/Attributes.lean

diff --git a/DocGen4.lean b/DocGen4.lean
index bc6d9b6..e91e7c7 100644
--- a/DocGen4.lean
+++ b/DocGen4.lean
@@ -9,3 +9,4 @@ import DocGen4.Load
 import DocGen4.ToHtmlFormat
 import DocGen4.IncludeStr
 import DocGen4.Output
+import DocGen4.Attributes
diff --git a/DocGen4/Attributes.lean b/DocGen4/Attributes.lean
new file mode 100644
index 0000000..474e175
--- /dev/null
+++ b/DocGen4/Attributes.lean
@@ -0,0 +1,110 @@
+import Lean
+
+namespace DocGen4
+
+open Lean Meta
+
+-- The following is probably completely overengineered but I love it
+class ValueAttr (attrKind : Type → Type) where
+  getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
+
+structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
+  {α : Type}
+  attr : attrKind α
+  [str : ToString α]
+  [inhab : Inhabited α]
+
+def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+  let val ← EnumAttributes.getValue attr env decl
+  some (toString val)
+
+instance : ValueAttr EnumAttributes where
+  getValue := enumGetValue
+
+def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+  let val ← ParametricAttribute.getParam attr env decl
+  some (attr.attr.name.toString ++ " " ++ toString val)
+
+instance : ValueAttr ParametricAttribute where
+  getValue := parametricGetValue
+
+abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
+abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
+
+def tagAttributes : Array TagAttribute := #[IR.UnboxResult.unboxAttr, neverExtractAttr, Elab.Term.elabWithoutExpectedTypeAttr, SynthInstance.inferTCGoalsRLAttr, matchPatternAttr]
+
+deriving instance Repr for Compiler.InlineAttributeKind
+deriving instance Repr for Compiler.SpecializeAttributeKind
+
+open Compiler in
+instance : ToString InlineAttributeKind where
+  toString kind :=
+    match kind with
+    | InlineAttributeKind.inline => "inline"
+    | InlineAttributeKind.noinline => "noinline"
+    | InlineAttributeKind.macroInline => "macroInline"
+    | InlineAttributeKind.inlineIfReduce => "inlineIfReduce"
+
+open Compiler in
+instance : ToString SpecializeAttributeKind where
+  toString kind :=
+    match kind with
+    | SpecializeAttributeKind.specialize => "specialize"
+    | SpecializeAttributeKind.nospecialize => "nospecialize"
+
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨Compiler.specializeAttrs⟩]
+
+instance : ToString ExternEntry where
+  toString entry :=
+    match entry with
+    | ExternEntry.adhoc `all => ""
+    | ExternEntry.adhoc backend => s!"{backend} adhoc"
+    | ExternEntry.standard `all fn => fn
+    | ExternEntry.standard backend fn => s!"{backend} {fn}"
+    | ExternEntry.inline backend pattern => s!"{backend} inline {String.quote pattern}"
+    -- TODO: The docs in the module dont specific how to render this
+    | ExternEntry.foreign backend fn  => s!"{backend} foreign {fn}"
+
+instance : ToString ExternAttrData where
+  toString data := (data.arity?.map toString |>.getD "") ++ String.intercalate " " (data.entries.map toString)
+
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩]
+
+def getTags (decl : Name) : MetaM (Array String) := do
+  let env ← getEnv
+  pure $ tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (λ t => t.attr.name.toString)
+
+def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
+  let env ← getEnv
+  pure $ va.getValue attr env decl
+
+def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
+  let env ← getEnv
+  let mut res := #[]
+  for attr in attrs do
+    if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
+      res := res.push val
+  pure res
+
+def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
+def getParametricValues (decl : Name) : MetaM (Array String) := getValues decl parametricAttributes
+
+def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
+  let insts ← getDefaultInstances className
+  for (inst, prio) in insts do
+    if inst == decl then
+      return some $ s!"defaultInstance {prio}"
+  pure none
+
+def hasSimp (decl : Name) : MetaM (Bool) := do
+  let thms ← simpExtension.getTheorems
+  pure $ thms.isLemma decl
+
+def getAllAttributes (decl : Name) : MetaM (Array String) := do
+  let tags ← getTags decl
+  let enums ← getEnumValues decl
+  let parametric ← getParametricValues decl
+  let simp := if ←hasSimp decl then #["simp"] else #[]
+  pure $ simp ++ tags ++ enums ++ parametric
+
+end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 94d7827..eef3186 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -72,7 +72,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-  let doc_html ← match doc with
+  let docHtml ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
   | DocInfo.classInfo i => classToHtml i
@@ -81,15 +81,23 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   | DocInfo.classInductiveInfo i => classInductiveToHtml i
   | _ => pure #[]
 
+  let attrs := doc.getAttrs
+  let attrsHtml :=
+    if attrs.size > 0 then
+      let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
+      #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+    else
+      #[]
+
   pure
     <div «class»="decl" id={doc.getName.toString}>
       <div «class»={doc.getKind}>
         <div «class»="gh_link">
           <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
         </div>
-        -- TODO: Attributes
+        [attrsHtml]
         {←docInfoHeader doc}
-        [doc_html]
+        [docHtml]
       </div>
     </div>
 
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index cb3df71..8435845 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -10,6 +10,7 @@ import Std.Data.HashMap
 import Lean.Meta.SynthInstance
 
 import DocGen4.Hierarchy
+import DocGen4.Attributes
 
 namespace DocGen4
 
@@ -29,6 +30,7 @@ structure Info extends NameInfo where
   args : Array Arg
   doc : Option String
   declarationRange : DeclarationRange
+  attrs : Array String
   deriving Inhabited
 
 structure AxiomInfo extends Info where
@@ -151,7 +153,7 @@ 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 => pure $ Info.mk ⟨v.name, type⟩ args doc range.range
+  | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range (←getAllAttributes v.name)
   | none => panic! s!"{v.name} is a declaration without position"
 
 def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
@@ -223,6 +225,14 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
     pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable
 
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+  let info ← DefinitionInfo.ofDefinitionVal v
+  let some className := getClassName (←getEnv) v.type | unreachable!
+  if let some instAttr ← getDefaultInstance v.name className then
+    pure { info with attrs := info.attrs.push instAttr }
+  else
+    pure info
+
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
   match env.find? ctor with
@@ -322,11 +332,12 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
     if ← (isProjFn i.name) then
       pure none
     else
-      let info ← DefinitionInfo.ofDefinitionVal i
       if (←isInstance i.name) then
+        let info ← InstanceInfo.ofDefinitionVal i
         pure <| some <| instanceInfo info
       else
-        pure <| some <| definitionInfo info
+        let info ← DefinitionInfo.ofDefinitionVal i
+        pure <| some <| definitionInfo  info
   | ConstantInfo.inductInfo i =>
     let env ← getEnv
     if isStructure env i.name then
@@ -422,6 +433,17 @@ def getArgs : DocInfo → Array Arg
 | classInfo i => i.args
 | classInductiveInfo i => i.args
 
+def getAttrs : DocInfo → Array String
+| axiomInfo i => i.attrs
+| theoremInfo i => i.attrs
+| opaqueInfo i => i.attrs
+| definitionInfo i => i.attrs
+| instanceInfo i => i.attrs
+| inductiveInfo i => i.attrs
+| structureInfo i => i.attrs
+| classInfo i => i.attrs
+| classInductiveInfo i => i.attrs
+
 end DocInfo
 
 structure AnalyzerResult where
@@ -475,6 +497,4 @@ def process : MetaM AnalyzerResult := do
     importAdj := adj
   }
 
-
-
 end DocGen4