commit 89c3877933e1b5ebf93d2d232400ebfeab143340
Author: Leon Vatthauer <leon.vatthauer@fau.de>
Date:   Wed Apr 10 17:11:47 2024 +0100

    initial commit, some work done

diff --git a/intro.agdai b/intro.agdai
new file mode 100644
index 0000000..bab4116
Binary files /dev/null and b/intro.agdai differ
diff --git a/intro.lagda.md b/intro.lagda.md
new file mode 100644
index 0000000..30d023b
--- /dev/null
+++ b/intro.lagda.md
@@ -0,0 +1,82 @@
+# 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, 
+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.
+
+<!--
+```agda
+module intro where
+Type = Set
+private
+  variable 
+    A B C : Type
+open import Agda.Primitive
+```
+-->
+
+## Warmup
+
+Ziel dieses Kapitels ist es etwas Familiarität mit Agda zu gewinnen. 
+Wir werden vor allem bekanntes Wissen aus ThProg anwenden und hier implementieren.
+
+### 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).
+
+Applikation in Agda ist klar, einfach das hintereinanderschreiben von Termen, Abstraktion wird geschrieben als 'λ x → t'.
+
+
+### Aufgabe 1
+Definiere die Identitätsfunktion
+
+```agda
+id : ∀ {A : Type} → A → A
+-- Erklärung des Typs:
+-- Der Allquantor funktioniert wie in System F, nur hat der Typ über den wir quantifizieren ebenfalls einen Typ! (Den Typ 'Type' der Typen)
+id = _
+```
+
+### Aufgabe 2
+Definiere die Komposition zweier Funktionen
+```agda
+_∘_ : ∀ {A B C : Type} → (g : B → C) → (f : A → B) → A → C
+_∘_ = _
+```
+
+## Induktive Datentypen
+Agda implementiert induktive Datentypen genau so wie wir sie in ThProg kennengelernt haben, d.h. wir definieren einen Datentypen, indem wir seine Konstruktoren angeben. Ein paar Beispiele:
+
+### Natürliche Zahlen
+```agda
+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!
+```
+
+#### Aufgabe 3
+Definiere die Additionsfunktion auf natürlichen Zahlen
+```agda
+add : ℕ → ℕ → ℕ
+add n m = _
+```
+
+Definiere die Prädezessorfunktion
+#### Aufgabe 4
+```agda
+pred : ℕ → ℕ
+pred n = _
+```
+
+#### Aufgabe 4
+Definiere eine Subtraktionsfunktion
+```agda
+sub : ℕ → ℕ → ℕ
+sub n m = _
+```
\ No newline at end of file
diff --git a/systemF.agdai b/systemF.agdai
new file mode 100644
index 0000000..d9c3603
Binary files /dev/null and b/systemF.agdai differ
diff --git a/systemF.lagda.md b/systemF.lagda.md
new file mode 100644
index 0000000..db2ddd1
--- /dev/null
+++ b/systemF.lagda.md
@@ -0,0 +1,13 @@
+## Recall: System F
+```agda
+ℕ : Set₁
+ℕ = ∀ {A} → (A → A) → A → A
+zero : ℕ
+zero = λ f x → x
+suc : ℕ → ℕ
+suc = λ n f x → f (n f x)
+fold : ∀ {A} → (A → A) → A → ℕ → A
+fold = λ f x n → n f x
+-- add : ℕ → ℕ → ℕ
+-- add = λ n → fold suc n
+```
\ No newline at end of file