coqtop – Online in der Cloud

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