feat: Sidenotes (leanprover#30)

This will allow many TODOs to be resolved

Main.lean

@@ -11,7 +11,7 @@ def main :=
 where
   config := {
     extraFiles := [("static", "static")],
-    extraCss := ["/static/theme.css", "/static/inter/inter.css", "/static/firacode/fira_code.css", "/static/katex/katex.min.css"],
+    extraCss := ["/static/colors.css", "/static/theme.css", "/static/inter/inter.css", "/static/firacode/fira_code.css", "/static/katex/katex.min.css"],
     extraJs := ["/static/katex/katex.min.js", "/static/math.js"]
     emitTeX := false
     emitHtmlSingle := false

Manual/Language/InductiveTypes.lean

@@ -10,16 +10,16 @@ open Lean.Parser.Command («inductive» «structure» declValEqns computedField)
 #doc (Manual) "Inductive Types" =>
 
 {deftech}_Inductive types_ are the primary means of introducing new types to Lean.
-While {tech}[universes] and {tech}[functions] are built-in primitives that could not be added by users, every other {tech}[canonical] {TODO}[Harmonize terminology: "type constructor" is probably better] type former in Lean is an inductive type.
+While {tech}[universes] and {tech}[functions] are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms universes, functions, and inductive types..
 Inductive types are specified by their {deftech}_type constructors_ {index}[type constructor] and their {deftech}_constructors_; {index}[constructor] their other properties are derived from these.
 Each inductive type has a single type constructor, which may take both {tech}[universe parameters] and ordinary parameters.
 Inductive types may have any number of constructors; these constructors introduce new values whose types are headed by the inductive type's type constructor.
 
 Based on the type constructor and the constructors for an inductive type, Lean derives a {deftech}_recursor_{index}[recursor]{see "recursor"}[eliminator].
 Logically, recursors represent induction principles or elimination rules; computationally, they represent primitive recursive computations.
 The termination of recursive functions is justified by translating them into uses of the recursors, so Lean's kernel only needs to perform type checking of recursor applications, rather than including a separate termination analysis.
-Lean additionally produces a number of helper constructions based on the recursor, which are used elsewhere in the system.
-{TODO}[Sidebar note: "recursor" is always used, even for non-recursive types]
+Lean additionally produces a number of helper constructions based on the recursor,{margin}[The term _recursor_ is always used, even for non-recursive datatypes.] which are used elsewhere in the system.
+
 
 _Structures_ are a special case of inductive types that have exactly one constructor.
 When a structure is declared, Lean generates helpers that enable additional language features to be used with the new structure.

Manual/Meta.lean

@@ -14,6 +14,7 @@ import Manual.Meta.Basic
 import Manual.Meta.Example
 import Manual.Meta.Figure
 import Manual.Meta.Lean
+import Manual.Meta.Marginalia
 import Manual.Meta.Syntax
 
 open Lean Elab
@@ -86,6 +87,8 @@ span.TODO {
   display: inline;
   position: relative;
   float: right;
+  clear: right;
+  margin-top: 1rem;
   width: 15vw;
   margin-right: -17vw;
   color: red;

Manual/Meta/Marginalia.lean

@@ -0,0 +1,85 @@
+import Verso
+import Verso.Doc.ArgParse
+import Verso.Doc.Elab.Monad
+import VersoManual
+import Verso.Code
+
+namespace Manual
+
+open Lean Elab
+open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
+open SubVerso.Highlighting Highlighted
+
+def Inline.margin : Inline where
+  name := `Manual.margin
+
+@[role_expander margin]
+def margin : RoleExpander
+  | args, inlines => do
+    ArgParse.done.run args
+    let content ← inlines.mapM elabInline
+    pure #[← `(Doc.Inline.other Inline.margin #[$content,*])]
+
+@[inline_extension margin]
+def margin.descr : InlineDescr where
+  traverse _ _ _ := do
+    pure none
+  toTeX := none
+  extraCss := [r#"
+.marginalia .note {
+  position: relative;
+  padding: 0.5rem;
+}
+/* Wide viewport */
+@media (min-width: 1400px) {
+.marginalia .note {
+  float: right;
+  clear: right;
+  margin-right: -19vw;
+  width: 15vw;
+  margin-top: 1rem;
+}
+}
+
+.marginalia:hover, .marginalia:hover .note, .marginalia:has(.note:hover) {
+  background-color: var(--lean-accent-light-blue);
+}
+
+/* Narrow viewport */
+@media (max-width: 1400px) {
+.marginalia .note {
+  float: right;
+  clear: right;
+  width: 40%;
+  margin: 1rem 0;
+  margin-left: 5%;
+}
+}
+body {
+  counter-reset: margin-note-counter;
+}
+.marginalia .note {
+  counter-increment: margin-note-counter;
+}
+.marginalia .note::before {
+  content: counter(margin-note-counter) ".";
+  position: absolute;
+  vertical-align: baseline;
+  font-size: 0.9em;
+  font-weight: bold;
+  left: -3rem;
+  width: 3rem;
+  text-align: right;
+}
+.marginalia::after {
+  content: counter(margin-note-counter);
+  vertical-align: super;
+  font-size: 0.7em;
+  font-weight: bold;
+  margin-right: 0.5em;
+}
+"#]
+  toHtml :=
+    open Verso.Output.Html in
+    some <| fun goI _ _ content  => do
+      pure {{<span class="marginalia"><span class="note">{{← content.mapM goI}}</span></span>}}

static/colors.css

@@ -0,0 +1,32 @@
+/* CSS variables for each Lean branding color */
+:root {
+    /* Main color palette */
+    --lean-black: #000000;
+    --lean-white: #ffffff;
+    --lean-blue: #0073a3;
+
+    /* Accent color palette */
+    /* This light blue should only be used as a background, and any text
+    on it should be black to ensure sufficient contrast. */
+    --lean-accent-light-blue: #b0c5cd;
+    /* This orange should be used only as an accent in small amounts. No
+    small type. Bold subhead or larger for typography.*/
+    --lean-accent-orange: #f15732;
+
+    /* Non-branding colors */
+    /* These colors should never be used as actual brand colors, but they
+    are complementary to our colors and can be used for elements in
+    presentations or charts or other peripheral materials. They are
+    only to be used as an accent or a complementary design element,
+    never as Lean branding. */
+    --lean-compl-orangered: #F15732;
+    --lean-compl-yellow: #FDC05F;
+    --lean-compl-green: #699E88;
+    --lean-compl-bluegray: #A9C7C9;
+    --lean-compl-darkgray: #354140;
+    --lean-compl-gray: #96A0A5;
+    --lean-compl-pink: #F05665;
+    --lean-compl-lightpink: #F7A8B0;
+    --lean-compl-darkblue: #005E7D;
+    --lean-compl-turquoise: #48C6E2;
+}

static/theme.css

@@ -2,8 +2,6 @@
     --verso-structure-font-family: "Inter", Helvetica, Arial, sans-serif;
     --verso-text-font-family: "Inter", Helvetica, Arial, sans-serif;
     --verso-code-font-family: "Fira Code", monospace;
-    --lean-blue: #0073a3;
-    --lean-light-blue: #98b2c0;
     --verso-toc-background-color: var(--lean-blue);
 }
 
@@ -30,7 +28,7 @@ h1, h2 {
 
 h3 {
     font-weight: 700;
-    color: var(--lean-light-blue);
+    color: var(--lean-accent-light-blue);
 }
 
 h4 {