From da7f00753b3e2c0eec3ea59d3ba593c08a9dffd4 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 12 May 2023 18:29:02 -0600 Subject: [PATCH] Common coloring across definitions/axioms/statements. --- Bookshelf/Apostol/Chapter_1_11.tex | 10 +++++----- Bookshelf/Enderton/Chapter_0.tex | 2 +- Common/Real/Geometry/Area.lean | 2 +- Common/Real/Geometry/Area.tex | 2 +- Common/Real/Sequence/Arithmetic.tex | 2 +- Common/Real/Sequence/Geometric.tex | 2 +- DocGen4/Output/Index.lean | 19 +++++++------------ preamble.tex | 18 ++++++++---------- 8 files changed, 25 insertions(+), 32 deletions(-) diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex index d6504b4..53120b6 100644 --- a/Bookshelf/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -132,7 +132,7 @@ $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$. \end{proof} -\subsection*{\proceeding{Exercise 4d}}% +\subsection*{\partial{Exercise 4d}}% \label{sub:exercise-4d} $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$ @@ -148,7 +148,7 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$ \end{proof} -\subsection*{\proceeding{Exercise 4e}}% +\subsection*{\partial{Exercise 4e}}% \label{sub:exercise-4e} $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$ @@ -164,7 +164,7 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$ \end{proof} -\section*{\proceeding{Exercise 5}}% +\section*{\partial{Exercise 5}}% \label{sec:exercise-5} The formulas in Exercises 4(d) and 4(e) suggest a generalization for @@ -389,7 +389,7 @@ Derive this result by a geometric argument, counting lattice points in a right \end{proof} -\subsection*{\proceeding{Exercise 7b}}% +\subsection*{\partial{Exercise 7b}}% \label{sub:exercise-7b} Derive the result analytically as follows: @@ -432,7 +432,7 @@ Now apply Exercises 4(a) and (b) to the bracket on the right. \end{proof} -\section*{\proceeding{Exercise 8}}% +\section*{\partial{Exercise 8}}% \label{sec:exercise-8} Let $S$ be a set of points on the real line. diff --git a/Bookshelf/Enderton/Chapter_0.tex b/Bookshelf/Enderton/Chapter_0.tex index 2e16866..6fa198c 100644 --- a/Bookshelf/Enderton/Chapter_0.tex +++ b/Bookshelf/Enderton/Chapter_0.tex @@ -10,7 +10,7 @@ \header{Useful Facts About Sets}{Herbert B. Enderton} -\section*{\proceeding{Lemma 0A}}% +\section*{\unverified{Lemma 0A}}% \label{sec:lemma-0a} Assume that $\langle x_1, \ldots, x_m \rangle = diff --git a/Common/Real/Geometry/Area.lean b/Common/Real/Geometry/Area.lean index a7cf711..f9eb3b8 100644 --- a/Common/Real/Geometry/Area.lean +++ b/Common/Real/Geometry/Area.lean @@ -94,7 +94,7 @@ axiom rectangle_measurable (R : Rectangle) axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle) : area (rectangle_measurable R) = R.width * R.height -/-! ## Exhaustion property +/-! ## Exhaustion Property Let `Q` be a set that can be enclosed between two step regions `S` and `T`, so that (1.1) `S ⊆ Q ⊆ T`. If there is one and only one number `k` which satisfies diff --git a/Common/Real/Geometry/Area.tex b/Common/Real/Geometry/Area.tex index 31ab25d..60a9aeb 100644 --- a/Common/Real/Geometry/Area.tex +++ b/Common/Real/Geometry/Area.tex @@ -71,7 +71,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$. \end{axiom} -\section*{\proceeding{Exhaustion Property}}% +\section*{\partial{Exhaustion Property}}% \label{sec:exhaustion-property} Let $Q$ be a set that can be enclosed between two step regions $S$ and $T$, so diff --git a/Common/Real/Sequence/Arithmetic.tex b/Common/Real/Sequence/Arithmetic.tex index c7d58c2..c782c03 100644 --- a/Common/Real/Sequence/Arithmetic.tex +++ b/Common/Real/Sequence/Arithmetic.tex @@ -8,7 +8,7 @@ \begin{document} -\section{\proceeding{Sum of Arithmetic Series}}% +\section{\unverified{Sum of Arithmetic Series}}% \label{sec:sum-arithmetic-series} Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. diff --git a/Common/Real/Sequence/Geometric.tex b/Common/Real/Sequence/Geometric.tex index 5cafa53..83db8b9 100644 --- a/Common/Real/Sequence/Geometric.tex +++ b/Common/Real/Sequence/Geometric.tex @@ -8,7 +8,7 @@ \begin{document} -\section{\proceeding{Sum of Geometric Series}}% +\section{\unverified{Sum of Geometric Series}}% \label{sec:sum-geometric-series} Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 5877829..24344f5 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -37,23 +37,18 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <| status:

diff --git a/preamble.tex b/preamble.tex index 4951f14..c2e8813 100644 --- a/preamble.tex +++ b/preamble.tex @@ -47,22 +47,20 @@ % Status % ======================================== -% Indicates a statement corresponds to an axiom or definition. There must exist -% a corresponding `axiom` or `def` in Lean. +% Used for statements encoded in both LaTeX and Lean. \DeclareRobustCommand{\defined}[1]{% - \texorpdfstring{\color{darkgray}\faParagraph\ #1}{#1}} + \texorpdfstring{\color{teal}\faParagraph\ #1}{#1}} -% Indicates a statement has a complete proof in both LaTeX *and* Lean. +% Used for statements proven in both LaTeX and Lean. \DeclareRobustCommand{\verified}[1]{% \texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}} -% Indicates a statement has not been completely proven in either LaTeX or -% Lean (or both). Progress is currently being made to correct this though. -\DeclareRobustCommand{\proceeding}[1]{% - \texorpdfstring{\color{magenta}\faDotCircle[regular]\ #1}{#1}} +% Used for statements proven or encoded in LaTeX but not yet in Lean. +\DeclareRobustCommand{\partial}[1]{% + \texorpdfstring{\color{magenta}\faPencil*\ #1}{#1}} -% A catch-all status for anything that doesn't fit the above categories. -% Incomplete definitions, proofs only conducted in LaTeX, etc. belong here. +% A catch-all for anything that doesn't fit the above categories. Incomplete +% definitions, statements without proof, etc. belong here. \DeclareRobustCommand{\unverified}[1]{% \texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}}