Dies ist der Befehl coqide.byte, der im kostenlosen OnWorks-Hosting-Provider über eine unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, Windows-Online-Emulator oder MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
coqide - Die grafische Oberfläche des Coq Proof Assistant
ZUSAMMENFASSUNG
Koqid [ Optionen ]
BESCHREIBUNG
Koqid ist eine grafische gtk-Schnittstelle für den Coq-Proof-Assistenten.
Informationen zur befehlszeilenorientierten Verwendung von Coq finden Sie unter coqtop(1) ; für den chargenorientierten Einsatz von Coq, siehe
coqc(1).
OPTIONAL
-h Zeigen Sie die vollständige Liste der akzeptierten Optionen an Koqid.
-I dir, -einschließen dir
Fügen Sie das Verzeichnis dir im Include-Pfad hinzu.
-R dir coqdir
Physisches rekursiv abbilden dir zu logisch coqdir.
-Quelle Fügen Sie Quellverzeichnisse im Include-Pfad hinzu.
-ist f, -Eingangszustand f
Zustand auslesen von f.coq.
-Nein ist Beginnen Sie mit einem leeren Zustand.
-Ausgangszustand f
Zustand in Datei schreiben f.coq.
-load-ml-Objekt f
ML-Objektdatei laden f.
-load-ml-Quelle f
ML-Datei laden f.
-l f, -load-vernac-source f
Coq-Datei laden f.v (Laden f.).
-lv f, -load-vernac-source-verbose f
Coq-Datei laden f.v (Ausführliches laden f.).
-Load-Vernac-Objekt f
Coq-Objektdatei laden f.vo.
-benötigen f
Coq-Objektdatei laden f.vo und importieren Sie es (Erforderlich f.).
-kompilieren f
Coq-Datei kompilieren f.v (impliziert -Charge).
-kompilieren-ausführlich f
Coq-Datei ausführlich kompilieren f.v (impliziert -Charge).
-opt Führen Sie die native Codeversion von Coq oder Coq_SearchIsos aus.
-Byte Führen Sie die Bytecode-Version von Coq oder Coq_SearchIsos aus.
-wo Drucken Sie den Standardbibliotheksspeicherort von Coq und beenden Sie ihn.
-v Coq-Version drucken und beenden.
-q Überspringen Sie das Laden der rcfile.
-init-Datei f
Setzen Sie die rcfile auf f.
-Charge Batch-Modus (beendet direkt nach dem Parsen der Argumente).
-Stiefel Boot-Modus (impliziert -q und -Charge).
-emacs Teilt Coq mit, dass es unter Emacs ausgeführt wird.
-Dump-Glob f
Globalisierungen in Datei ablegen f (zu verwenden von coqdoc(1)).
-Imprädikativ-Set
Set sort Set imprädikativ.
-nicht belastungssicher
Laden Sie keine undurchsichtigen Beweise in den Speicher.
-xml Exportieren Sie XML-Dateien entweder in die im Verzeichnis verwurzelte Hierarchie
COQ_XML_LIBRARY_ROOT (falls gesetzt) oder auf stdout (wenn nicht gesetzt).
Verwenden Sie coqide.byte online mit den onworks.net-Diensten
