Checkpoint upto 5.2.1

pufferffish · Feb 29, 2024 · 2d859f5 · 2d859f5
1 parent 5d33cdb
commit 2d859f5
Show file tree

Hide file tree

Showing 8 changed files with 246 additions and 178 deletions.
diff --git a/papers/icfp24/arxiv-sort.tex b/papers/icfp24/arxiv-sort.tex
@@ -131,6 +131,17 @@
 %% microtypography
 \usepackage{microtype}
 
+%% space saving magic macro
+\usepackage[
+  all=normal,
+  paragraphs,
+  floats,
+  wordspacing,
+  charwidths,
+  mathdisplays,
+  indent,
+]{savetrees}
+
 %% custom macros
 \usepackage{hott}
 \usepackage{math}

diff --git a/papers/icfp24/free-commutative-monoids.tex b/papers/icfp24/free-commutative-monoids.tex
diff --git a/papers/icfp24/free-monoids.tex b/papers/icfp24/free-monoids.tex
@@ -327,8 +327,9 @@ \subsection{Array}\label{mon:array}
     and $((f \comp S) \oplus g)(k)$ reduces to $g(k - n)$ by definition, therefore they are equal.
 \end{proof}
 
-\begin{definition}
-    We define the $\ext{(\blank)}$ on $f : A \to X$:
+\begin{definition}[Universal extension (fold)]
+    Given a monoid $\mathfrak{X}$, and a map $f : A \to X$,
+    we define $\ext{f} : \Array(A) \to X$, by induction on the length of the array:
     \begin{align*}
         \ext{f}(0 , g)    & = e                                    \\
         \ext{f}(S(n) , g) & = f(g(0)) \mult \ext{f}(n , g \circ S)

diff --git a/papers/icfp24/icfp24-sort-strip.pdf b/papers/icfp24/icfp24-sort-strip.pdf
diff --git a/papers/icfp24/icfp24-sort-strip.tex b/papers/icfp24/icfp24-sort-strip.tex
@@ -131,6 +131,17 @@
 %% microtypography
 \usepackage{microtype}
 
+%% space saving magic macro
+\usepackage[
+  all=normal,
+  paragraphs,
+  floats,
+  wordspacing,
+  charwidths,
+  mathdisplays,
+  indent,
+]{savetrees}
+
 %% custom macros
 \usepackage{hott}
 \usepackage{math}

diff --git a/papers/icfp24/icfp24-sort-submission.pdf b/papers/icfp24/icfp24-sort-submission.pdf
diff --git a/papers/icfp24/icfp24-sort.pdf b/papers/icfp24/icfp24-sort.pdf
diff --git a/papers/icfp24/math.sty b/papers/icfp24/math.sty
@@ -36,6 +36,7 @@
 \newcommand{\str}[1]{\mathfrak{#1}}
 
 \newcommand{\ext}[1]{{#1}^{\sharp}}
+\newcommand{\exthat}[1]{{#1}^{\bar{\sharp}}}
 
 \newcommand{\eq}{\term{eq}}
 \newcommand{\fv}{\term{fv}}