coq-tex - Online sa Cloud

PROGRAMA:

NAME

coq-tex - Iproseso ang mga pariralang Coq na naka-embed sa LaTeX file

SINOPSIS

coq-tex [ -o output-file ] [ -n lapad ng linya ] [ -mage larawan ng coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -maliit ] input-file ...

DESCRIPTION

Ang coq-tex Kinukuha ng filter ang mga parirala ng Coq na naka-embed sa mga LaTeX file, sinusuri ang mga ito, at
ipasok ang kinalabasan ng pagsusuri pagkatapos ng bawat parirala.

Tatlong LaTeX environment ang ibinigay para isama ang Coq code sa mga input file:

coq_example
Ang mga parirala sa pagitan ng \begin{coq_example} at \end{coq_example} ay sinusuri at
kinopya sa output file. Ang bawat parirala ay sinusundan ng tugon ng
toplevel loop.

coq_example*
Ang mga parirala sa pagitan ng \begin{coq_example*} at \end{coq_example*} ay sinusuri at
kinopya sa output file. Ang mga tugon ng toplevel loop ay itatapon.

coq_eval
Ang mga parirala sa pagitan ng \begin{coq_eval} at \end{coq_eval} ay tahimik na sinusuri.
Hindi sila kinopya sa output file, at ang mga tugon ng toplevel loop
ay itinatapon.

Ang resultang LaTeX code ay nakaimbak sa file file.v.tex kung ang input file ay may pangalan ng
ang form file.tex, kung hindi, ang pangalan ng output file ay ang pangalan ng input file
na may nakadugtong na `.v.tex'.

Ang mga file na ginawa ng coq-tex maaaring direktang iproseso ng LaTeX. Parehong ang mga parirala ng Coq
at ang toplevel na output ay naka-typeset sa typewriter font.

Opsyon

-o output-file
Tukuyin ang pangalan ng isang file kung saan iimbak ang LaTeX output. Isang gitling `-'
nagiging sanhi ng pagpi-print ng LaTeX output sa karaniwang output.

-n lapad ng linya
Itakda ang lapad ng linya. Ang default ay 72 character. Ang mga tugon ng toplevel
ang loop ay nakatiklop kung mas mahaba sila kaysa sa lapad ng linya. Walang ginagawang pagtitiklop sa
ang Coq input text.

-mage larawan ng coq
Dahilan ang file larawan ng coq na isasagawa upang suriin ang mga parirala ng Coq. Bilang default,
ito ang utos coqtop nang hindi tinukoy ang anumang landas na ginagamit upang suriin
ang mga parirala ng Coq.

-w Maging sanhi ng mga linya na nakatiklop sa isang space character hangga't maaari, na iniiwasan ang mga pagbawas ng salita
sa output. Bilang default, ang pagtitiklop ay nangyayari sa lapad ng linya, anuman ang salita
hiwa

-v Verbose mode. Ini-print ang mga sagot ng Coq sa karaniwang output. Kapaki-pakinabang upang makita
mga pagkakamali sa mga parirala ng Coq.

-sl Slanted mode. Ang mga sagot ng Coq ay nakasulat sa isang slanted font.

-hrule Pahalang na mga linya mode. Ang mga bahagi ng Coq ay nakasulat sa pagitan ng dalawang pahalang na linya.

-maliit Maliit na font mode. Ang mga bahagi ng Coq ay nakasulat sa isang mas maliit na font.

MGA CAVEATS

Ang mga \begin... at \end... na mga parirala ay dapat umupo sa isang linya nang mag-isa, na walang mga character
bago ang backslash o pagkatapos ng closing brace. Ang bawat parirala ng Coq ay dapat wakasan ng
`.' sa dulo ng isang linya. Tinatanggap ang blangkong espasyo sa pagitan ng `.' at ang bagong linya, ngunit anuman
ibang karakter ay magiging sanhi ng coq-tex na huwag pansinin ang dulo ng parirala, na magreresulta sa isang
maling pag-shuffling ng mga tugon sa mga parirala. (Ang mga tugon na ``nahuhuli''.)

Gumamit ng coq-tex online gamit ang mga serbisyo ng onworks.net