diff --git a/common/header.tex b/common/header.tex
index 6d57fe7..40c5258 100644
--- a/common/header.tex
+++ b/common/header.tex
@@ -84,6 +84,7 @@
 \newcommand{\Γ}{\Gamma}
 \newcommand{\τ}{\tau}
 \newcommand{\σ}{\sigma}
+\newcommand{\λ}{\lambda}
 \newcommand{\recleq}{\sqsubsetleq}
 \newcommand{\discrete}[2]{\left\{ #1, \ldots{}, #2 \right\}}
 
diff --git a/grammar/expressions.tex b/grammar/expressions.tex
index b0d4c29..2bb4b9a 100644
--- a/grammar/expressions.tex
+++ b/grammar/expressions.tex
@@ -3,7 +3,7 @@
   <e> ::=
     \x/ \| \c/
     \alt \e/.\a/ \| \e/.\a/ or \e/
-    \alt \p/:\e/ \| \e/ \e/
+    \alt $\λ$\p/.\e/ \| \e/ \e/
     \alt \{ \e/ = \e/ \}
     \alt with \e/; \e/
     \alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
diff --git a/grammar/values.tex b/grammar/values.tex
index 0270313..39b6ab9 100644
--- a/grammar/values.tex
+++ b/grammar/values.tex
@@ -3,7 +3,7 @@
 
   <v> ::=
     \c/
-    \alt \p/:\e/
+    \alt $\λ$\p/.\e/
     \alt \{ \v/ = \e/ \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/ \}
     \alt Cons(\e/, \e/) \| nil
 \end{grammar}
diff --git a/semantics/semantics.tex b/semantics/semantics.tex
index 43de78e..80592ab 100644
--- a/semantics/semantics.tex
+++ b/semantics/semantics.tex
@@ -10,8 +10,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
     \dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/}{$e$}{}
     \dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/ or $e'$}{$e$}{}
     \dstepa{$v.s \text{ or } e'$}{$e'$}{if $\v/ \neq$ \{ \s/ = \e/; $\ldots{}$ \}}
-    \dstepa{$(x:e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
-    \dstepa{$(p:e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
+    \dstepa{$(\λ x.e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
+    \dstepa{$(\λ p.e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
     \dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \} ; \e/}{
       \e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
     }{}