Setup

Warum Agda?

• Verdeutlicht Curry-Howard-Korrespondenz
  

    →-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
• Optisch Nah zu Mathematik dank Unicode-Support, z. B.: DFA

Installation von Agda

Agda compiler

Hinweise zur Installation sind unter diesen Quellen zu finden:

• Offizielle Agda-Doc
• Weitere Anleitungen: Setup bei PLFA
• 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 verwenden. Die standard library ist im unten referenzierten nix-flake bereits enthalten.

• Klonen Sie die agda-stdlib in Version 2.3 in einen Pfad Ihrer Wahl, z. B.:
  

  $ mkdir -p ~/.agda/repos/
  $ git clone -b v2.3 https://github.com/agda/agda-stdlib.git ~/.agda/repos/stdlib
  

• Tragen Sie den Pfad in der ~/.agda/libraries ein:
  

  $ mkdir -p ~/.agda/
  $ echo ~/.agda/repos/stdlib/standard-library.agda-lib > ~/.agda/libraries
  

• Erstellen Sie eine ~/.agda/default und tragen Sie die standard library als default ein:
  

  $ echo standard-library > ~/.agda/libraries
  

Installation via Nix

Anstelle der manuellen Installation, kann man unter den meisten Distributionen Agda via des Packetmanagers nix installieren. Hierfür trägt man

experimental-features = nix-command flakes

in die ~/.config/nix/nix.conf ein und lädt die Dateien

• flake.nix
• flake.lock

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

Agda Quellcode herunterladen