Dies ist der Befehl coqc, 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
coqc – Der Coq Proof Assistant-Compiler
ZUSAMMENFASSUNG
coqc [ General Hahn Optionen ] Datei
BESCHREIBUNG
coqc ist der Batch-Compiler für den Coq Proof Assistant. Die Optionen sind grundsätzlich die
wie coqtop(1). Datei.v ist die zu kompilierende umgangssprachliche Datei. Datei muss erst gebildet werden
mit den Zeichen `a` bis `Z`, `0`-`9` oder `_` und muss mit einem Buchstaben beginnen. Der
Der Compiler erzeugt eine Objektdatei Datei.vo.
Informationen zur interaktiven Nutzung von Coq finden Sie unter coqtop(1).
OPTIONAL
coqc ist ein Skript, das einfach ausgeführt wird coqtop mit Option -kompilieren es akzeptiert die gleichen Optionen
as coqtop.
-Bild Kasten
- Kasten als Basiswert coqtop anstelle der Standardeinstellung.
-verbose
Drucken Sie die kompilierte Datei auf der Standardausgabe.
Nutzen Sie coqc online über die Dienste von onworks.net
