r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix spacing and update links to new tabs.

finite-set-exercises
Joshua Potter 2023-08-01 12:51:47 -06:00
parent 8b1da10ef1
commit fc3b659613
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output/Index.lean
View File

@ -51,12 +51,12 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
<li> <li>
<span style="color:olive">Olive statements </span> are reserved for <span style="color:olive">Olive statements </span> are reserved for
statements, theorems, lemmas, etc. that have been proven in LaTeX statements, theorems, lemmas, etc. that have been proven in LaTeX
and will <i>not</i> be proven in Lean. and will <i>not </i> be proven in Lean.
</li> </li>
<li> <li>
<span style="color:fuchsia">Fuchsia statements </span> are reserved <span style="color:fuchsia">Fuchsia statements </span> are reserved
for definitions, axioms, statements, theorems, lemmas, etc. that for definitions, axioms, statements, theorems, lemmas, etc. that
have been proven or encoded in LaTeX and <i>will</i> be encoded in have been proven or encoded in LaTeX and <i>will </i> be encoded in
Lean. Lean.
</li> </li>
<li> <li>

2
DocGen4/Output/Navbar.lean
View File

@ -16,7 +16,7 @@ open scoped DocGen4.Jsx
def moduleListFile (file : NameExt) : BaseHtmlM Html := do def moduleListFile (file : NameExt) : BaseHtmlM Html := do
let contents := let contents :=
if file.ext == .pdf then if file.ext == .pdf then
<span>{s!"🗎 {file.getString!} (<a class=\"pdf\" href={← moduleNameExtToLink file}>pdf</a>)"}</span> <span>{s!"🗎 {file.getString!} (<a class=\"pdf\" target=\"_blank\" href={← moduleNameExtToLink file}>pdf</a>)"}</span>
else else
<a href={← moduleNameExtToLink file}>{file.getString!}</a> <a href={← moduleNameExtToLink file}>{file.getString!}</a>
return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}> return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}>