coq-tex - Online di Cloud

PROGRAM:

NAMA

coq-tex - Memproses frasa Coq yang disematkan dalam file LaTeX

RINGKASAN

coq-tex [ -o berkas keluaran ] [ -n lebar garis ] [ -gambar gambar-coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -kecil ] file masukan ...

DESKRIPSI

coq-tex filter mengekstrak frasa Coq yang disematkan dalam file LaTeX, mengevaluasinya, dan
masukkan hasil evaluasi setelah setiap frase.

Tiga lingkungan LaTeX disediakan untuk menyertakan kode Coq dalam file input:

coq_contoh
Frasa antara \begin{coq_example} dan \end{coq_example} dievaluasi dan
disalin ke dalam file keluaran. Setiap frase diikuti oleh respon dari
lingkaran tingkat atas.

coq_contoh*
Frasa antara \begin{coq_example*} dan \end{coq_example*} dievaluasi dan
disalin ke dalam file keluaran. Tanggapan dari loop tingkat atas dibuang.

coq_eval
Frasa antara \begin{coq_eval} dan \end{coq_eval} dievaluasi secara diam-diam.
Mereka tidak disalin ke file output, dan tanggapan dari loop tingkat atas
dibuang.

Kode LaTeX yang dihasilkan disimpan dalam file fillet.v.tex jika file input memiliki nama
formulir fillet.tex, jika tidak, nama file output adalah nama file input
dengan `.v.tex' ditambahkan.

File yang dihasilkan oleh coq-tex dapat langsung diproses oleh LaTeX. Kedua frasa Coq
dan output tingkat atas diketik dalam font mesin tik.

PILIHAN

-o berkas keluaran
Tentukan nama file tempat output LaTeX akan disimpan. Tanda hubung `-'
menyebabkan keluaran LaTeX tercetak pada keluaran standar.

-n lebar garis
Mengatur lebar garis. Standarnya adalah 72 karakter. Tanggapan dari tingkat atas
loop dilipat jika lebih panjang dari lebar garis. Tidak ada pelipatan yang dilakukan pada
teks masukan Coq.

-gambar gambar-coq
Penyebab file gambar-coq akan dieksekusi untuk mengevaluasi frase Coq. Secara default,
ini perintahnya coqtop tanpa menentukan jalur apa pun yang digunakan untuk mengevaluasi
frase Coq.

-w Menyebabkan garis dilipat pada karakter spasi bila memungkinkan, menghindari pemotongan kata
dalam keluaran. Secara default, pelipatan terjadi pada lebar garis, terlepas dari kata
memotong.

-v Modus verbose. Mencetak jawaban Coq pada output standar. Berguna untuk mendeteksi
kesalahan dalam frasa Coq.

-sl Modus miring. Jawaban Coq ditulis dengan huruf miring.

-hrule Modus garis horizontal. Bagian Coq ditulis di antara dua garis horizontal.

-kecil Modus huruf kecil. Bagian Coq ditulis dalam font yang lebih kecil.

PERINGATAN

Frasa \begin... and \end... harus berada dalam satu baris sendiri, tanpa karakter
sebelum garis miring terbalik atau setelah kurung kurawal penutup. Setiap frase Coq harus diakhiri dengan
`.' di akhir sebuah baris. Ruang kosong diterima antara `.' dan baris baru, tetapi apa saja
karakter lain akan menyebabkan coq-tex mengabaikan akhir frasa, menghasilkan
pengocokan jawaban yang salah ke dalam frasa. (Tanggapan ``tertinggal di belakang''.)

Gunakan coq-tex online menggunakan layanan onworks.net