diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index dbbe838..4ae69a5 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/parts/02_typing/00_intro.tex b/semester4/fmfp/parts/02_typing/00_intro.tex
index 61c7319..f7b23d5 100644
--- a/semester4/fmfp/parts/02_typing/00_intro.tex
+++ b/semester4/fmfp/parts/02_typing/00_intro.tex
@@ -1,3 +1,6 @@
 A great type system is essential for all programming languages, but especially so for functional programming languages.
 
 The issue however is that the problem of deciding which expressions are good and which ones aren't is undecidable.
+
+Thus, languages only allow a subset of good expressions.
+The goal is to make the type system as unrestrictive as possible while still retaining quick, static code analysis.
diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex b/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex
index f520cac..74a71cd 100644
--- a/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex
+++ b/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex
@@ -2,3 +2,10 @@
 This is a stripped down version of Haskell, used here to explore the type system Haskell uses
 
 \subsubsection{Syntax}
+Programs are terms, the core is the lambda-calculus, where $\cV$ is the set of variables and $\Z$ the set of integers:
+\[
+    t :: = \cV \divider (\lambda x. t) \divider (t_1 t_2) \divider True \divider False \divider (\textbf{iszero } t) \divider \Z \divider (t_1 + t_2) \divider t_1 * t_2 
+    \divider \textbf{if } t_0 \textbf{ then } t_1 \textbf{ else } t_2 \divider (t_1, t_2) \divider (\textbf{fst } t) \divider (\textbf{snd } t)
+\]
+
+It is easily possible to add additonal syntax and types and we employ syntactic sugar, such as omitting parenthesis.