diff --git a/Makefile b/Makefile
index c48f538..1222297 100644
--- a/Makefile
+++ b/Makefile
@@ -27,4 +27,5 @@ push: all
 	mv -T agda-intro public
 
 Everything.agda:
+	rm -f src/Everything.agda
 	git ls-files | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort >> src/Everything.agda
diff --git a/src/Everything.agda b/src/Everything.agda
index 20ef564..86bc2be 100644
--- a/src/Everything.agda
+++ b/src/Everything.agda
@@ -1,5 +1 @@
 import Intro
-import Intro
-import Intro
-import Intro
-import Intro
diff --git a/src/Intro.lagda.md b/src/Intro.lagda.md
index c0bd29e..3e83fc0 100644
--- a/src/Intro.lagda.md
+++ b/src/Intro.lagda.md
@@ -1,6 +1,6 @@
 # Funktionale Programmierung in Agda
 In dieser Datei werden wir einen kleinen Blick in funktionale Programmierung mit Agda wagen. 
-Agda ist eine funktionale Programmiersprache wie Haskell, 
+Agda ist eine funktionale Programmiersprache deren Syntax der von Haskell sehr ähnlich ist, 
 jedoch besitzt Agda ein deutlich ausdrucksstärkeres Typsystem durch sogenannte *dependent types*.
 Das sind Typen welche von Termen der Programmiersprache abhängen können, aber dazu in späteren Kapiteln mehr.
 
@@ -24,11 +24,12 @@ Wir werden vor allem bekanntes Wissen aus ThProg anwenden und hier implementiere
 ### Recall: Lambda-Kalkül
 Der (ungetypte) Lambda-Kalkül ist die Grundlage jeder funktionalen Programmiersprache.
 Ein Term des Lambda-Kalküls ist entweder
-- Eine Variable x ∈ V
-- Eine Applikation zweier Lambda Terme t₁t₂
-- Eine Lambda-Abstraktion λx.t, wobei x ∈ V und t Term.
 
-Diese drei Komponenten finden wir deshalb in jeder funktionalen Programmiersprache, wobei in der Regel Syntaxzucker für Lambda-Abstraktionen angeboten wird (die übliche Funktionsnotation).
+- Eine Variable *x ∈ V*
+- Eine Applikation zweier Lambda Terme *t₁ t₂*
+- Eine Lambda-Abstraktion *λx.t*, wobei *x ∈ V* und *t* Term.
+
+Diese drei Komponenten finden wir deshalb in jeder funktionalen Programmiersprache, wobei in der Regel Syntaxzucker für Lambda-Abstraktionen angeboten wird. D.h. *f x = b* ist Syntaxzucker für *λ x → b*.
 
 Applikation in Agda ist klar, einfach das hintereinanderschreiben von Termen, Abstraktion wird geschrieben als 'λ x → t'.
 
@@ -57,9 +58,6 @@ Agda implementiert induktive Datentypen genau so wie wir sie in ThProg kennengel
 data 𝔹 : Type where
   tt : 𝔹
   ff : 𝔹
-{-# BUILTIN BOOL  𝔹  #-}
-{-# BUILTIN TRUE  tt #-}
-{-# BUILTIN FALSE ff #-}
 ```
 
 #### Aufgabe 3
@@ -95,21 +93,27 @@ foldb t s b = _
 data ℕ : Type where
   zero : ℕ
   succ : ℕ → ℕ
-{-# BUILTIN NATURAL ℕ #-} -- Hierdurch können wir einfach '0, 1, 2, ...' statt 'zero, succ zero, succ (succ zero), ...' schreiben, wir bekommen aber **keine** Funktionen wie z.B. Addition geschenkt!
+{-# BUILTIN NATURAL ℕ #-} -- Hierdurch können wir einfach '0, 1, 2, ...' statt 'zero, succ zero, succ (succ zero), ...' schreiben. Wir bekommen aber **keine** Funktionen wie z.B. Addition geschenkt!
 ```
 
 #### Aufgabe 7
-Definiere die Additionsfunktion auf natürlichen Zahlen.
+Definiere Funktionen zur Addition und Subtraktion natürlicher Zahlen.
 ```agda
 add : ℕ → ℕ → ℕ
 add n m = _
+
+sub : ℕ → ℕ → ℕ
+sub n m = _
 ```
 
 #### Aufgabe 8
-Definiere eine Subtraktionsfunktion.
+Definiere Funktionen `odd` und `even`, welche testen ob eine natürliche Zahl gerade oder ungerade ist.
 ```agda
-sub : ℕ → ℕ → ℕ
-sub n m = _
+odd : ℕ → 𝔹
+odd n = _
+
+even : ℕ → 𝔹
+even n = _
 ```
 
 #### Aufgabe 9
@@ -119,6 +123,28 @@ foldn : ∀ {C : Type} → C → (C → C) → ℕ → C
 foldn c h n = _ 
 ```
 
+#### Optionale Aufgaben
+
+##### Optionale Aufgabe 1
+Definiere `add'` und `sub'` mittels `foldn` (*ohne* pattern matching).
+```agda
+add' : ℕ → ℕ → ℕ
+add' = _
+
+sub' : ℕ → ℕ → ℕ
+sub' = _
+```
+
+##### Optionale Aufgabe 2
+Definiere `odd'` und `even'` mittels `foldn` (*ohne* pattern matching).
+```agda
+odd' : ℕ → 𝔹
+odd' = _
+
+even' : ℕ → 𝔹
+even' = _
+```
+
 ### Listen
 
 ```agda