removed agdai, add nix, add exercises

.envrc

@@ -0,0 +1 @@
+use flake

.gitignore

@@ -0,0 +1,2 @@
+*.agdai
+.direnv/

Makefile

@@ -0,0 +1,30 @@
+.PHONY: all clean pandoc Everything.agda
+
+all: agda
+	make pandoc
+
+pandoc: public/*.md
+	@$(foreach file,$^, \
+		pandoc $(file) -s --to=html+TEX_MATH_DOLLARS --mathjax -c Agda.css -o $(file:.md=.html) ; \
+	)
+
+agda: Everything.agda
+	agda --html --html-dir=public src/Everything.agda --html-highlight=auto -i.
+	rm -f public/Agda.css
+	cp Agda.css public/Agda.css
+
+clean:
+	rm -f Everything.agda
+	rm -rf public/*
+	find . -name '*.agdai' -exec rm \{\} \;
+
+# push compiled html to my cip directory
+push: all
+	chmod +w public/Agda.css
+	rm -rf agda-intro
+	mv -T public agda-intro
+	scp -r agda-intro hy84coky@cip1d1.cip.cs.fau.de:.www/
+	mv -T agda-intro public
+
+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

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1712588820,
+        "narHash": "sha256-y31s5idk3jMJMAVE4Ud9AdI7HT3CgTAeMTJ0StqKN7Y=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "d272ca50d1f7424fbfcd1e6f1c9e01d92f6da167",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,15 @@
+{
+  description = "Flake for using/compiling this project.";
+
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.11";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem
+      (system:
+        let pkgs = nixpkgs.legacyPackages.${system}; in
+        {
+          devShells.default = import ./shell.nix { inherit pkgs; };
+        }
+      );
+}

shell.nix

@@ -0,0 +1,10 @@
+{ pkgs ? import <nixpkgs> { } }:
+with pkgs;
+mkShell {
+  buildInputs = [ agda ];
+
+  shellHook = ''
+    # ...
+  '';
+}
+

src/Intro.lagda.md

@@ -6,7 +6,7 @@ Das sind Typen welche von Termen der Programmiersprache abhängen können, aber
 
 <!--
 ```agda
-module intro where
+module Intro where
 Type = Set
 private
   variable 
@@ -33,8 +33,7 @@ Applikation in Agda ist klar, einfach das hintereinanderschreiben von Termen, Ab
 
 
 ### Aufgabe 1
-Definiere die Identitätsfunktion
-
+Definiere die Identitätsfunktion.
 ```agda
 id : ∀ {A : Type} → A → A
 -- Erklärung des Typs:
@@ -43,7 +42,7 @@ id = _
 ```
 
 ### Aufgabe 2
-Definiere die Komposition zweier Funktionen
+Definiere die Komposition zweier Funktionen.
 ```agda
 _∘_ : ∀ {A B C : Type} → (g : B → C) → (f : A → B) → A → C
 _∘_ = _
@@ -52,6 +51,44 @@ _∘_ = _
 ## 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:
 
+### Booleans
+```agda
+data 𝔹 : Type where
+  tt : 𝔹
+  ff : 𝔹
+{-# BUILTIN BOOL  𝔹  #-}
+{-# BUILTIN TRUE  tt #-}
+{-# BUILTIN FALSE ff #-}
+```
+
+#### Aufgabe 3
+Definiere die Funktion `flip`, welche einen logischen Wert invertiert.
+```agda
+flip : 𝔹 → 𝔹
+flip b = _
+```
+
+#### Aufgabe 4
+Definiere die Funktion `and`.
+```agda
+and : 𝔹 → 𝔹 → 𝔹
+and b₁ b₂ = _
+```
+
+#### Aufgabe 5
+Definiere die Funktion `if then else`.
+```agda
+if_then_else_ : ∀ {A : Type} → 𝔹 → A → A → A
+if b then t else s = _
+```
+
+#### Aufgabe 6
+Definiere die Fold-Funktion auf booleans.
+```agda
+foldb : ∀ {C : Type} → C → C → 𝔹 → C
+foldb t s b = _
+```
+
 ### Natürliche Zahlen
 ```agda
 data ℕ : Type where
@@ -60,23 +97,61 @@ data ℕ : Type where
 {-# 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
+#### Aufgabe 7
+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
+#### Aufgabe 8
+Definiere eine Subtraktionsfunktion.
 ```agda
 sub : ℕ → ℕ → ℕ
 sub n m = _
+```
+
+#### Aufgabe 9
+Definiere die Fold-Funktion auf natürlichen Zahlen.
+```agda
+foldn : ∀ {C : Type} → C → (C → C) → ℕ → C
+foldn c h n = _ 
+```
+
+### Listen
+
+```agda
+data List (A : Type) : Type where
+  nil : List A
+  _∷_ : A → List A → List A
+{-# BUILTIN LIST List #-}
+infixr 5 _∷_
+```
+
+#### Aufgabe 10
+Definiere die `length` Funktion.
+```agda
+length : ∀ {A : Type} → List A → ℕ
+length xs = _
+```
+
+#### Aufgabe 11
+Definiere die `filter` Funktion.
+```agda
+filter : ∀ {A : Type} → (A → 𝔹) → List A → List A
+filter f xs = _
+```
+
+#### Aufgabe 12
+Definiere die `map` Funktion.
+```agda
+map : ∀ {A B : Type} → (A → B) → List A → List B
+map f xs = _
+```
+
+#### Aufgabe 13
+Definiere die Fold-Funktion für Listen.
+```agda
+foldr : ∀ {C : Type} → C → (A → C → C) → List A → C
+foldr c h xs = _
 ```