-
Notifications
You must be signed in to change notification settings - Fork 36
/
Inductive.lean
39 lines (33 loc) · 1.11 KB
/
Inductive.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
def instancesForToHtml (typeName : Name) : HtmlM Html := do
pure
<details «class»="instances">
<summary>Instances For</summary>
<ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
</details>
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := c.name.componentsRev.head!.toString
let name := c.name.toString
if let some doc := c.doc then
let renderedDoc ← docStringToHtml doc
pure
<li class="constructor" id={name}>
<div class="inductive_ctor_doc">[renderedDoc]</div>
{shortName} : [←infoFormatToHtml c.type]
</li>
else
pure
<li class="constructor" id={name}>
{shortName} : [←infoFormatToHtml c.type]
</li>
def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
pure #[constructorsHtml]
end Output
end DocGen4