Dies ist der Befehl coqtop, 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
coqtop – Das Top-Level-System des Coq Proof Assistant
ZUSAMMENFASSUNG
coqtop [ Optionen ]
BESCHREIBUNG
coqtop ist das Top-Level-System von Coq für die interaktive Nutzung. Es liest Sätze auf der
Standardeingabe und druckt Ergebnisse auf der Standardausgabe.
Informationen zur stapelorientierten Verwendung von Coq finden Sie unter coqc(1).
OPTIONAL
-H, --help
Hilfe. Sie erhalten die vollständige Liste der von coqtop akzeptierten Optionen.
-I ist, --enthalten dir
Verzeichnis hinzufügen dir im Include-Pfad
-R dir coqdir
physikalische rekursiv abbilden dir zu logisch coqdir
-oben coqdir
Legen Sie den Namen der obersten Ebene fest coqdir statt Top
-Eingangszustand Dateiname, -ist Dateinamen
Status aus Datei lesen Dateiname.coq
-Nein ist Beginnen Sie mit einem leeren Anfangszustand
-AusgangszustandDateinamen
Zustand in Datei schreiben Dateiname.coq
-load-ml-Objekt Dateinamen
ML-Objektdatei laden Dateiname
-load-ml-Quelle Dateinamen
ML-Datei laden Dateinamen
-load-vernac-source Dateiname, -l Dateinamen
Coq-Datei laden Dateiname.v (Dateiname laden.)
-load-vernac-source-verbose Dateiname, -lv Dateinamen
Laden Sie ausführlich die Coq-Datei Dateiname.v (Ausführlichen Dateinamen laden.)
-Load-Vernac-Objekt Dateinamen
Laden Sie die Coq-Objektdatei Dateiname.vo
-benötigen Dateinamen
Laden Sie die Coq-Objektdatei Dateiname.vo und importieren Sie es (Importdateiname erforderlich).
-kompilieren Dateinamen
Coq-Datei kompilieren Dateiname.v (impliziert -Charge )
-kompilieren-ausführlich Dateinamen
Coq-Datei ausführlich kompilieren Dateiname.v (impliziert -Charge )
-opt Führen Sie die Native-Code-Version von Coq aus
-Byte Führen Sie die Bytecode-Version von Coq aus
-wo Geben Sie den Standardspeicherort der Coq-Bibliothek aus und verlassen Sie ihn
-v Coq-Version drucken und beenden
-q Überspringen Sie das Laden der RC-Datei
-init-Datei Dateinamen
Setzen Sie die RC-Datei auf Dateinamen
-Charge Batch-Modus (wird unmittelbar nach dem Parsen der Argumente beendet)
-Stiefel Bootmodus (impliziert -q und -Charge )
-emacs teilt Coq mit, dass es unter Emacs ausgeführt wird
-Dump-Glob Dateinamen
Dump Globalisierungen in Datei f (zu verwenden von coqdoc(1) )
-mit-geoproof (ja|nein)
um spezielle Funktionen für Geoproof innerhalb von Coqide zu (de)aktivieren (Standard ist ja )
-Imprädikativ-Set
set sort Imprädikativ festlegen
-nicht belastungssicher
Laden Sie keine undurchsichtigen Proofs in den Speicher
-xml Exportieren Sie XML-Dateien entweder in die im Verzeichnis verwurzelte Hierarchie
$COQ_XML_LIBRARY_ROOT (falls gesetzt) oder an stdout (falls nicht gesetzt)
-Qualität
Verbessern Sie die Lesbarkeit der Beweisbegriffe, die durch einige Taktiken erzeugt werden
Nutzen Sie coqtop online über die Dienste von onworks.net
