Dit is de opdracht coq-tex die kan worden uitgevoerd in de gratis hostingprovider van OnWorks met behulp van een van onze meerdere gratis online werkstations zoals Ubuntu Online, Fedora Online, Windows online emulator of MAC OS online emulator
PROGRAMMA:
NAAM
coq-tex - Verwerk Coq-zinnen die zijn ingebed in LaTeX-bestanden
KORTE INHOUD
coq-tex [ -o output-bestand ] [ -n lijnbreedte ] [ -beeld coq-afbeelding ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -klein ] Invoer bestand ...
PRODUCTBESCHRIJVING
De coq-tex filter extraheert Coq-zinnen die zijn ingebed in LaTeX-bestanden, evalueert ze, en
plaats na elke zin de uitkomst van de evaluatie.
Er zijn drie LaTeX-omgevingen beschikbaar om Coq-code in de invoerbestanden op te nemen:
coq_voorbeeld
De zinnen tussen \begin{coq_example} en \end{coq_example} worden geëvalueerd en
gekopieerd naar het uitvoerbestand. Elke zin wordt gevolgd door het antwoord van de
lus op het hoogste niveau.
coq_voorbeeld*
De zinnen tussen \begin{coq_example*} en \end{coq_example*} worden geëvalueerd en
gekopieerd naar het uitvoerbestand. De antwoorden van de lus op het hoogste niveau worden verwijderd.
coq_eval
De zinnen tussen \begin{coq_eval} en \end{coq_eval} worden stil geëvalueerd.
Ze worden niet gekopieerd naar het uitvoerbestand en de antwoorden van de lus op het hoogste niveau
worden weggegooid.
De resulterende LaTeX-code wordt in het bestand opgeslagen filet.v.tex als het invoerbestand de naam heeft
het formulier filet.tex, anders is de naam van het uitvoerbestand de naam van het invoerbestand
met `.v.tex' toegevoegd.
De bestanden geproduceerd door coq-tex kan rechtstreeks door LaTeX worden verwerkt. Beide Coq-zinnen
en de uitvoer op het hoogste niveau wordt in het typemachinelettertype gezet.
OPTIES
-o output-bestand
Geef de naam op van een bestand waarin de LaTeX-uitvoer moet worden opgeslagen. Een streepje `-'
zorgt ervoor dat de LaTeX-uitvoer op standaarduitvoer wordt afgedrukt.
-n lijnbreedte
Stel de lijndikte in. De standaardwaarde is 72 tekens. De reacties van het hoogste niveau
lus worden gevouwen als ze langer zijn dan de lijnbreedte. Er wordt niet gevouwen
de Coq-invoertekst.
-beeld coq-afbeelding
Oorzaak het bestand coq-afbeelding uit te voeren om de Coq-zinnen te evalueren. Standaard,
dit is de opdracht koktop zonder een pad op te geven dat wordt gebruikt om te evalueren
de Coq-zinnen.
-w Zorg ervoor dat regels waar mogelijk op een spatie worden gevouwen, waarbij woordafbrekingen worden vermeden
in de uitvoer. Standaard vindt vouwen plaats op de lijnbreedte, ongeacht het woord
bezuinigingen.
-v Uitgebreide modus. Drukt de Coq-antwoorden af op de standaarduitvoer. Handig om te detecteren
fouten in Coq-zinnen.
-sl Schuine modus. De Coq-antwoorden zijn geschreven in een schuin lettertype.
-hrule Horizontale lijnenmodus. De Coq-delen zijn tussen twee horizontale lijnen geschreven.
-klein Kleine lettertypemodus. De Coq-delen zijn in een kleiner lettertype geschreven.
WAARSCHUWINGEN
De zinnen \begin... en \end... moeten op zichzelf staan, zonder tekens
vóór de backslash of na het sluitende accolade. Elke Coq-zin moet worden beëindigd door
`.' aan het einde van een regel. Er wordt een spatie tussen `.' geaccepteerd en de nieuwe regel, maar welke dan ook
Een ander teken zorgt ervoor dat coq-tex het einde van de zin negeert, wat resulteert in een
onjuiste verdeling van de antwoorden in de zinnen. (De antwoorden ``blijven achter''.)
Gebruik coq-tex online met behulp van onworks.net-services