Dies ist der Befehl gallina, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
Gallina – extrahiert Spezifikationen aus Coq-Volkssprachendateien
ZUSAMMENFASSUNG
Henne [ - ] [ -stdout ] [ -keine Kommentare ] Datei ...
BESCHREIBUNG
Henne Nimmt Coq-Dateien als Argumente und erstellt die entsprechenden Spezifikationsdateien.
Die Coq-Datei foo.v gibt der Spezifikationsdatei einen Namen foo.g. Das Suffix „.g“ steht
für Gallina.
Zu diesem Zweck entfernt Gallina alle Befehle, die einem „Theorem“, „Lemma“, „Fakt“ folgen.
„Bemerkung“ oder „Ziel“-Anweisung, bis ein Befehl „Abbrechen“, „Speichern“, „Qed.“ erreicht wird.
„Definiert.“ oder „Beweis <...>.“ Es entfernt auch jeden „Hinweis“, jede „Syntax“, „Immediate“ oder
Befehl „Transparent“.
Dateien ohne das Suffix .v werden ignoriert.
OPTIONAL
-stdout
Druckt das Ergebnis auf der Standardausgabe.
- Die Coq-Quelle wird über die Standardeingabe übernommen. Das Ergebnis wird auf der Standardausgabe gedruckt.
-keine Kommentare
Kommentare werden in der *.g-Datei entfernt.
ANMERKUNG
Verschachtelte Kommentare werden korrekt behandelt. Insbesondere jeder Befehl „Speichern“. oder „Abbruch“. In
ein Kommentar wird nicht berücksichtigt.
Nutzen Sie Gallina online über die Dienste von onworks.net
