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
  • [←infoFormatToHtml c]
  • +/-- +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