Ini ialah arahan coq-tex yang boleh dijalankan dalam penyedia pengehosan percuma OnWorks menggunakan salah satu daripada berbilang stesen kerja dalam talian percuma kami seperti Ubuntu Online, Fedora Online, emulator dalam talian Windows atau emulator dalam talian MAC OS.
JADUAL:
NAMA
coq-tex - Memproses frasa Coq dibenamkan dalam fail LaTeX
SINOPSIS
coq-tex [ -o fail keluaran ] [ -n lebar garis ] [ -imej imej coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -kecil ] fail input ...
DESCRIPTION
. coq-tex penapis mengekstrak frasa Coq yang dibenamkan dalam fail LaTeX, menilainya dan
masukkan hasil penilaian selepas setiap frasa.
Tiga persekitaran LaTeX disediakan untuk memasukkan kod Coq dalam fail input:
contoh_coq
Frasa antara \begin{coq_example} dan \end{coq_example} dinilai dan
disalin ke dalam fail output. Setiap frasa diikuti dengan respons daripada
gelung peringkat atas.
coq_example*
Frasa antara \begin{coq_example*} dan \end{coq_example*} dinilai dan
disalin ke dalam fail output. Respons gelung peringkat atas dibuang.
coq_eval
Frasa antara \begin{coq_eval} dan \end{coq_eval} dinilai secara senyap.
Mereka tidak disalin ke dalam fail output, dan respons gelung peringkat atas
dibuang.
Kod LaTeX yang terhasil disimpan dalam fail fail.v.tex jika fail input mempunyai nama
borang fail.tex, jika tidak, nama fail output ialah nama fail input
dengan `.v.tex' dilampirkan.
Fail yang dihasilkan oleh coq-tex boleh diproses terus oleh LaTeX. Kedua-dua frasa Coq
dan output peringkat atas adalah set taip dalam fon mesin taip.
PILIHAN
-o fail keluaran
Nyatakan nama fail di mana output LaTeX akan disimpan. Sengkang `-'
menyebabkan output LaTeX dicetak pada output standard.
-n lebar garis
Tetapkan lebar garisan. Lalai ialah 72 aksara. Maklum balas peringkat atasan
gelung dilipat jika ia lebih panjang daripada lebar garisan. Tiada lipatan dilakukan pada
teks input Coq.
-imej imej coq
Sebab fail imej coq untuk dilaksanakan untuk menilai frasa Coq. Secara lalai,
ini perintahnya coqtop tanpa menyatakan sebarang laluan yang digunakan untuk menilai
frasa Coq.
-w Menyebabkan garisan dilipat pada aksara ruang apabila boleh, mengelakkan pemotongan perkataan
dalam keluaran. Secara lalai, lipatan berlaku pada lebar garisan, tanpa mengira perkataan
pemotongan.
-v Mod bertele-tele. Mencetak jawapan Coq pada output standard. Berguna untuk mengesan
kesilapan dalam frasa Coq.
-sl Mod senget. Jawapan Coq ditulis dalam fon senget.
-hrule Mod garisan mendatar. Bahagian Coq ditulis di antara dua garis mendatar.
-kecil Mod fon kecil. Bahagian Coq ditulis dalam fon yang lebih kecil.
CATATAN
Frasa \begin... dan \end... mesti diletakkan pada satu baris dengan sendirinya, tanpa aksara
sebelum garis miring ke belakang atau selepas pendakap penutup. Setiap frasa Coq mesti ditamatkan oleh
`.' di hujung baris. Ruang kosong diterima antara `.' dan baris baharu, tetapi mana-mana
watak lain akan menyebabkan coq-tex mengabaikan penghujung frasa, mengakibatkan an
merombak jawapan yang salah ke dalam frasa. (Respons ``tertinggal''.)
Gunakan coq-tex dalam talian menggunakan perkhidmatan onworks.net