feat: show inductive constructor argument names

DocGen4/Output/Inductive.lean

@@ -8,27 +8,41 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
+/--
+Render an `Arg` as HTML, adding opacity effects etc. depending on what
+type of binder it has.
+-/
+def argToHtml (arg : Process.Arg) : HtmlM Html := do
+  let node ← infoFormatToHtml arg.binder
+  let inner := <span class="fn">[node]</span>
+  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+  if arg.implicit then
+    return <span class="impl_arg">{html}</span>
+  else
+    return html
+
 def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
   pure
     <details id={s!"instances-for-list-{typeName}"} «class»="instances-for-list">
         <summary>Instances For</summary>
         <ul class="instances-for-enum"></ul>
     </details>
 
-def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+def ctorToHtml (c : Process.ConstructorInfo) : HtmlM Html := do
   let shortName := c.name.componentsRev.head!.toString
   let name := c.name.toString
+  let args ← c.args.mapM argToHtml
   if let some doc := c.doc then
     let renderedDoc ← docStringToHtml doc name
     pure
       <li class="constructor" id={name}>
-        {shortName} : [← infoFormatToHtml c.type]
+        {shortName} [args] {" : "} [← infoFormatToHtml c.type]
         <div class="inductive_ctor_doc">[renderedDoc]</div>
       </li>
   else
     pure
       <li class="constructor" id={name}>
-        {shortName} : [← infoFormatToHtml c.type]
+        {shortName} [args] {" : "} [← infoFormatToHtml c.type]
       </li>
 
 def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do

DocGen4/Output/Module.lean

@@ -20,19 +20,6 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean Process
 
-/--
-Render an `Arg` as HTML, adding opacity effects etc. depending on what
-type of binder it has.
--/
-def argToHtml (arg : Arg) : HtmlM Html := do
-  let node ← infoFormatToHtml arg.binder
-  let inner := <span class="fn">[node]</span>
-  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
-  if arg.implicit then
-    return <span class="impl_arg">{html}</span>
-  else
-    return html
-
 /--
 Render the structures this structure extends from as HTML so it can be
 added to the top level.

DocGen4/Process/Base.lean

@@ -117,14 +117,19 @@ structure InstanceInfo extends DefinitionInfo where
   typeNames : Array Name
   deriving Inhabited
 
+/--
+Information about a constructor of an inductive type
+-/
+abbrev ConstructorInfo := Info
+
 /--
 Information about an `inductive` declaration
 -/
 structure InductiveInfo extends Info where
   /--
   List of all constructors of this inductive type.
   -/
-  ctors : List NameInfo
+  ctors : List ConstructorInfo
   isUnsafe : Bool
   deriving Inhabited
 
@@ -166,11 +171,6 @@ Information about a `class inductive` declaration.
 abbrev ClassInductiveInfo := InductiveInfo
 
 
-/--
-Information about a constructor of an inductive type
--/
-abbrev ConstructorInfo := Info
-
 /--
 A general type for informations about declarations.
 -/

DocGen4/Process/InductiveInfo.lean

@@ -12,15 +12,9 @@ namespace DocGen4.Process
 
 open Lean Meta 
 
-def getConstructorType (ctor : Name) : MetaM Expr := do
-  let env ← getEnv
-  match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => pure 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 ctors ← v.ctors.mapM (fun name => do NameInfo.ofTypedName name (← getConstructorType name))
+  let ctors ← v.ctors.mapM (fun name => do Info.ofConstantVal (← getConstInfoCtor name).toConstantVal)
   return {
     toInfo := info,
     ctors,

static/style.css

@@ -753,7 +753,7 @@ a:hover {
     transition: opacity 300ms ease-in;
 }
 
-.decl_header:not(:hover) .impl_arg {
+.decl_header:not(:hover) .impl_arg, .constructor:not(:hover) .impl_arg {
     opacity: 30%;
     transition: opacity 1000ms ease-out;
 }