lualatex -> xelatex

Makefile

@@ -19,7 +19,7 @@ main.pdf: main.tex $(GENERATED_LATEX)
 	latexmk \
 	  -output-directory=out \
 	  -pdf \
-	  -lualatex \
+	  -xelatex \
 	  -bibtex \
 	  -use-make \
 	  -interaction=nonstopmode \

context/nix/syntax-and-semantics.md

@@ -78,7 +78,7 @@ has a particular form, that needs a particular treatement).
   \begin{lstlisting}
 <expr> ::=
   <ident> | <constant>
-  | $\lambda$ <pattern>.<expr> | <expr> <expr>
+  | λ <pattern>.<expr> | <expr> <expr>
   | let <var-pattern> = <expr>; $\cdots$; <var-pattern> = <expr>; in <expr>
   | [ <expr> $\cdots$ <expr> ]
   | { <record-field>; $\cdots$; <record-field>; }

default.nix

@@ -14,7 +14,13 @@ stdenv.mkDerivation rec {
       biber
   ];
 
-  src = ./.;
+  src = builtins.filterSource (name: type:
+    let baseName = baseNameOf (toString name); in !(
+        (type == "directory" &&
+        (baseName == ".git" ||
+          baseName == "out"))))
+    ./.;
+
 
   installPhase = ''
     mkdir -p $out/nix-support

main.tex

@@ -52,9 +52,9 @@
   literate={% replace strings with symbols
     {->}{{$\to$}}{1}
     {<>}{{$\diamond$}}{1}
-    {lambda}{{$\lambda$}}{1}
-    {tau}{{\ensuremath{\tau}}}{1}
-    {rho}{{\ensuremath{\rho}}}{1}
+    {λ}{{$\lambda$}}{1}
+    {τ}{{\ensuremath{\tau}}}{1}
+    {ρ}{{\ensuremath{\rho}}}{1}
     {tin}{{$\in$}}{1}
     {\&}{{$\wedge$}}{1}
     {AND}{{$\wedge$}}{1}
@@ -83,15 +83,14 @@
 
 \lstMakeShortInline{°}
 
-\usepackage{myunicode}
-
 % Some useful macros
 \catcode`τ=13
 \catcode`λ=13
+\catcode`ρ=13
 \catcode`Γ=13
 \newcommand{λ}{\ensuremath{\lambda}}
-\newcommand{τ}{\ensuremath{\tau}}
-\newcommand{τ}{\ensuremath{\tau}}
+\newcommand{τ}{tau}
+\newcommand{\τ}{\ensuremath{\tau}}
 \newcommand{\lbl}[1]{\text{(\emph{#1})}}
 % Subtyping
 \newcommand{\subtype}{\leq}

nix-light/description.md

@@ -36,7 +36,7 @@ Moreover, we often write `{ x1 = e1; $\cdots$; xn = en }` as a shortcut for
   \begin{lstlisting}
 <expr> ::= <ident> | <constant>
   | <expr>.<expr> | <expr>.<expr> or <expr>
-  | $\lambda$<pattern>.<expr> | <expr> <expr>
+  | λ <pattern>.<expr> | <expr> <expr>
   | let <var-pattern> = <expr>; $\cdots{}$; <var-pattern> = <expr>; in <expr>
   | Cons (<expr>, <expr>)
   | { <ident> = <expr> } | {} | <expr> <> ... <> <expr>

typing/lambda-calculus.md

@@ -91,7 +91,7 @@ The arguments have to be annotated explicitly (or `?` is assumed). Thus the
 inference of an abstraction is rather simple.
 
 The check is somehow more complex. The idea is that to check that an expression
-$\lambda p.e$ admits the type $\τ$ under the hypothesis $\Gamma$ we must check
+$λ p.e$ admits the type $\τ$ under the hypothesis $\Gamma$ we must check
 that each arrow type $\sigma_1 \rightarrow \sigma_2$ "contained" in $\τ$ is
 admitted by the expression, which means that under the hypothesis $\Gamma;
 \tmatch{\sigma_1}{p}$, $e$ admits the type $\sigma_2$.

typing/lambda-inference-rules.tex

@@ -10,7 +10,7 @@
     \and\inferrule{%
       \Gamma;\tmatch{\accept{p}}{p} \tinfer e : \τ
     }{%
-      \Gamma \tinfer \lambda p.e : \accept{p} \rightarrow \tau
+      \Gamma \tinfer λ p.e : \accept{p} \rightarrow \tau
     } \lbl{IAbs}
 
   \and\inferrule{%
@@ -18,7 +18,7 @@
     \forall \sigma_1 \rightarrow \sigma_2 \in \A(\tau), \\
       \Gamma;\tmatch{\sigma_1}{p} \tcheck e : \sigma_2
   }{%
-    \Gamma \tcheck \lambda p.e : \tau
+    \Gamma \tcheck λ p.e : \tau
   }\lbl{CAbs}