# Setup

## Warum Agda?

* Verdeutlicht Curry-Howard-Korrespondenz
  ```agda
  →-transitive : ∀ {A B C : Set} → (A → B) → (B → C) → (A → C)
  →-transitive = λ a→b b→c a → b→c (a→b a)
  ```

* Wenige aber dafür mächtige Sprach-Features.
* Erlaubt definition von Gleichungs-Reasoning: [Beispiel](https://arxiv.org/src/2602.16427v1/anc/html/Utils.html#2%5E%E2%8C%8Alog2n%E2%8C%8B-acc%E2%89%A4n)
* Optisch Nah zu Mathematik dank Unicode-Support, z. B.:
  [DFA](https://arxiv.org/src/2602.16427v1/anc/html/DFA.html)
  

## Installation von Agda

### Agda compiler

Hinweise zur Installation sind unter diesen Quellen zu finden:

* [Offizielle Agda-Doc](https://agda.readthedocs.io/en/latest/getting-started/installation.html)
* Weitere Anleitungen: [Setup bei PLFA](https://plfa.inf.ed.ac.uk/GettingStarted/)
* Installation via nix-flake (siehe unten)

### Standard-Library

In der VL werden wir zentrale Elemente zum Lerngewinn selbst definieren, aber im
Nachfolgenden dann die Definitionen aus der [Agda Standard
Library](https://github.com/agda/agda-stdlib) verwenden. Die standard library
ist im unten referenzierten nix-flake bereits enthalten.

* Klonen Sie die [agda-stdlib](https://github.com/agda/agda-stdlib.git) in Version 2.3 in einen Pfad Ihrer Wahl, z. B.:
  <pre>
$ mkdir -p ~/.agda/repos/
$ git clone -b v2.3 https://github.com/agda/agda-stdlib.git ~/.agda/repos/stdlib
</pre>
* Tragen Sie den Pfad in der `~/.agda/libraries` ein:
  <pre>
$ mkdir -p ~/.agda/
$ echo ~/.agda/repos/stdlib/standard-library.agda-lib > ~/.agda/libraries
</pre>

* Erstellen Sie eine `~/.agda/default` und tragen Sie die standard library als default ein:
  <pre>
$ echo standard-library > ~/.agda/libraries
</pre>


### Installation via Nix
Anstelle der manuellen Installation, kann man unter den meisten Distributionen Agda
via des Packetmanagers `nix` installieren. Hierfür trägt man
```ini
experimental-features = nix-command flakes
```
in die `~/.config/nix/nix.conf` ein und lädt die Dateien 

  - [flake.nix](https://arxiv.org/src/2602.16427v1/anc/flake.nix)
  - [flake.lock](https://arxiv.org/src/2602.16427v1/anc/flake.lock)

herunter. Dann erhält man mit `nix develop` in eine Shell mit installiertem Agda.