Wanted: Agda-Lückentextaufgabe

Ähnlich wie Cyp und Haskell-Lückentext. Lücken in Beweis/Programm sind zu füllen, aber andere Teile nicht zu ändern, so daß das Dokument schließlich akzeptiert wird.

Es sollte für Agda viel einfacher sein, da es die Lücken schon in der Sprache selbst gibt. Da muß "nur noch" der Vergleich der ASTs implementiert werden.

Genauer:

• es gibt Lücken für Ausdrücke, wir sollten aber auch erlauben (ggf. konfigurierbar durch Aufgabensteller)
• weitere Klauseln in einer Funktions-Definition (wenn sie Instanzen einer bereits hingeschriebenen sind)
• weitere Hilfsfunktionen?

Zu untersuchen ist, ob man Datei-Operationen braucht, oder Agda den Quelltext aus Data.Text lesen kann. Das sollte gehen, wenn keine weiteren Module benutzt werden? Auch ohne Standardbibliothek kann man viele Aufgaben stellen.