Dies ist der Befehl coq-tex, 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
coq-tex - Coq-Sätze verarbeiten, die in LaTeX-Dateien eingebettet sind
ZUSAMMENFASSUNG
coq-tex [ -o Ausgabedatei ] [ -n Linienbreite ] [ -Bild coq-Bild ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -klein ] Eingabedatei ...
BESCHREIBUNG
Die coq-tex filter extrahiert in LaTeX-Dateien eingebettete Coq-Phrasen, wertet sie aus und
Fügen Sie das Ergebnis der Bewertung nach jedem Satz ein.
Drei LaTeX-Umgebungen werden bereitgestellt, um Coq-Code in die Eingabedateien aufzunehmen:
coq_beispiel
Die Phrasen zwischen \begin{coq_example} und \end{coq_example} werden ausgewertet und
in die Ausgabedatei kopiert. Auf jeden Satz folgt die Antwort des
Schleife auf oberster Ebene.
coq_beispiel*
Die Phrasen zwischen \begin{coq_example*} und \end{coq_example*} werden ausgewertet und
in die Ausgabedatei kopiert. Die Antworten der Schleife der obersten Ebene werden verworfen.
coq_eval
Die Phrasen zwischen \begin{coq_eval} und \end{coq_eval} werden stillschweigend ausgewertet.
Sie werden nicht in die Ausgabedatei kopiert und die Antworten der Toplevel-Schleife
werden verworfen.
Der resultierende LaTeX-Code wird in der Datei gespeichert Datei.v.tex, wenn die Eingabedatei den Namen hat
die Form Datei.tex, ansonsten ist der Name der Ausgabedatei der Name der Eingabedatei
mit angehängtem `.v.tex'.
Die Dateien produziert von coq-tex kann direkt von LaTeX verarbeitet werden. Beide Coq-Sätze
und die Ausgabe auf oberster Ebene sind in Schreibmaschinenschrift gesetzt.
OPTIONAL
-o Ausgabedatei
Geben Sie den Namen einer Datei an, in der die LaTeX-Ausgabe gespeichert werden soll. Ein Strich `-'
bewirkt, dass die LaTeX-Ausgabe auf der Standardausgabe gedruckt wird.
-n Linienbreite
Legen Sie die Linienbreite fest. Der Standardwert beträgt 72 Zeichen. Die Antworten der obersten Ebene
Schleife werden gefaltet, wenn sie länger als die Linienbreite sind. Es wird keine Faltung durchgeführt auf
den Coq-Eingabetext.
-Bild coq-Bild
Ursache die Datei coq-Bild ausgeführt werden, um die Coq-Sätze auszuwerten. Standardmäßig,
das ist der Befehl coqtop ohne Angabe eines Pfades, der zur Auswertung verwendet wird
die Coq-Sätze.
-w Verhindern Sie, dass Zeilen nach Möglichkeit auf ein Leerzeichen gefaltet werden, um Wortkürzungen zu vermeiden
in der Ausgabe. Standardmäßig erfolgt die Faltung mit der Linienbreite, unabhängig vom Wort
Schnitte.
-v Ausführlicher Modus. Druckt die Coq-Antworten auf der Standardausgabe. Nützlich zu erkennen
Fehler in Coq-Phrasen.
-sl Schräger Modus. Die Coq-Antworten sind in schräger Schrift geschrieben.
-hrule Modus für horizontale Linien. Die Coq-Teile werden zwischen zwei horizontalen Linien geschrieben.
-klein Kleinschriftmodus. Die Coq-Teile sind in kleinerer Schrift geschrieben.
VORSICHTEN
Die Sätze \begin... und \end... müssen in einer eigenen Zeile stehen, ohne Zeichen
vor dem Backslash oder nach der schließenden Klammer. Jede Coq-Phrase muss mit abgeschlossen werden
`.' am Ende einer Zeile. Leerzeichen werden zwischen `.' akzeptiert. und der Zeilenumbruch, aber alle
ein anderes Zeichen bewirkt, dass coq-tex das Ende der Phrase ignoriert, was zu einem führt
falsches Mischen der Antworten in die Phrasen. (Die Antworten „hinken hinterher“.)
Nutzen Sie coq-tex online mit den onworks.net-Diensten