From fc3b659613a9572eded3172bc8d620b9ab84f1ce Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 1 Aug 2023 12:51:47 -0600 Subject: [PATCH] Fix spacing and update links to new tabs. --- DocGen4/Output/Index.lean | 4 ++-- DocGen4/Output/Navbar.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 536b43c..7033767 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -51,12 +51,12 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
  • Olive statements are reserved for statements, theorems, lemmas, etc. that have been proven in LaTeX - and will not be proven in Lean. + and will not be proven in Lean.
  • Fuchsia statements are reserved for definitions, axioms, statements, theorems, lemmas, etc. that - have been proven or encoded in LaTeX and will be encoded in + have been proven or encoded in LaTeX and will be encoded in Lean.
  • diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index cc39fac..7081e6d 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -16,7 +16,7 @@ open scoped DocGen4.Jsx def moduleListFile (file : NameExt) : BaseHtmlM Html := do let contents := if file.ext == .pdf then - {s!"🗎 {file.getString!} (pdf)"} + {s!"🗎 {file.getString!} (pdf)"} else {file.getString!} return