From e0bf4ad28c4187070410fbc67f01af03a3f22463 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 19 May 2022 21:07:44 +0200
Subject: [PATCH] doc: Output/Definition

---
 DocGen4/Output/Definition.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index 3e0b146..6be1639 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -7,12 +7,18 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean Widget
 
-/- This is basically an arbitrary number that seems to work okay. -/
+/-- This is basically an arbitrary number that seems to work okay. -/
 def equationLimit : Nat := 200
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
   pure <li class="equation">[←infoFormatToHtml c]</li>
 
+/--
+Attempt to render all `simp` equations for this definition. At a size
+defined in `equationLimit` we stop trying since they:
+- are too ugly to read most of the time
+- take too long
+-/
 def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml