Prepare use of minted

.gitignore

@@ -26,4 +26,7 @@
 __pycache__/
 
 /**/target
-/**/mir_dump
\ No newline at end of file
+/**/mir_dump
+
+/**/_minted*
+*.pygtex
\ No newline at end of file

preamble.tex

@@ -51,6 +51,10 @@
 ]{markdown}
 
 \usepackage{xcolor}
+\usepackage{minted}
+\setminted{autogobble, mathescape}
+
+
 \usepackage{listings}
 \lstdefinelanguage{Rust}{%
 sensitive,%

thesis/1-introduction.tex

@@ -656,46 +656,52 @@ Since the inception of set theory, mathematicians used \emph{set comprehension}
 
 \noindent which circumvents the paradox. \emph{Refinement types} are the type theoretic analogue to restricted comprehension. Some programming languages allow for refinement types. For example, in the Lean theorem prover, the introductory example would translate to
 
-\begin{lstlisting}
-{ n : nat // prime n }
--- Syntactic sugar for:
-subtype nat prime
-\end{lstlisting}
+\begin{listing}[H]
+    \begin{minted}[mathescape]{lean}
+        { n : $\BbbN$ // prime n }
+        -- Syntactic sugar for:
+        subtype nat prime
+    \end{minted}
+    \caption{Refinement types in Lean}
+    \label{lst:lean-subtype}
+\end{listing}
 
 \inline{subtype} is a type constructor, that is a generic type, with two arguments. The first argument \inline{nat} is a type, but the second argument \inline{prime} is a value of function type. Rust has limited support for types depending on values with \emph{const generics}, but it does not support functions as const generics, which means that refinement types can’t be implemented in Rust this way.\todo{More on full dependent types, Pi and Sigma types, lambda cube?} There have been proposals for introducing more const generic capabilities to Rust\footnote{\url{https://github.com/ticki/rfcs/blob/pi-types/text/0000-pi-types.md}}, but they are put into cold storage indefinitely. We can still imagine what the equivalent Rust code would be if it could be written:
 
-\begin{lstlisting}[language=Rust]
-struct Prop<const B: Bool>;
-
-impl<const B: bool> Prop<B> {
-    const fn new() -> Self {
-        if B {
-            Self
-        } else {
-            panic!()
+\begin{listing}
+    \begin{minted}{rust}
+        struct Prop<const B: Bool>;
+
+        impl<const B: bool> Prop<B> {
+            const fn new() -> Self {
+                if B {
+                    Self
+                } else {
+                    panic!()
+                }
+            }
         }
-    }
-}
 
-struct Subtype<T, const pred: fn(T) -> bool> {
-    val: T,
-    proof: Prop<pred(val)>
-}
-
-impl<T, const pred: fn(T) -> bool> Subtype<T, pred> {
-    const fn new(val: T) -> Self {
-        Self {
-            val,
-            proof: Prop::new::<pred(val)>()
+        struct Subtype<T, const pred: fn(T) -> bool> {
+            val: T,
+            proof: Prop<pred(val)>
         }
-    }
-}
 
-// Also implement `Deref` and `DerefMut` so that a
-// `Subtype<T, pred>` can be used in any place where a
-// `T` is expected.
+        impl<T, const pred: fn(T) -> bool> Subtype<T, pred> {
+            const fn new(val: T) -> Self {
+                Self {
+                    val,
+                    proof: Prop::new::<pred(val)>()
+                }
+            }
+        }
 
-\end{lstlisting}
+        // Also implement `Deref` and `DerefMut` so that a
+        // `Subtype<T, pred>` can be used in any place where a
+        // `T` is expected.
+    \end{minted}
+    \caption{The Rusty equivalent.}
+\end{listing}
 
 \noindent\inline{Prop} is a helper type which can only be created from a true value. We need this so that we can proof that \inline{val} makes \inline{prop} true. This would now allow us to create constants that have certain proven properties like in \autoref{lst:proven-const}.
 

thesis/thesis.tex

-% arara: lualatex
+% arara: lualatex: {shell: true}
 % arara: biber
-% arara: lualatex
-% arara: lualatex
+% arara: lualatex: {shell: true}
+% arara: lualatex: {shell: true}
 
 \documentclass[a4paper, oneside, article]{memoir}