.TH COQ\-TEX 1
.
.SH "نام (NAME)"
coq\-tex \- پردازش عبارت‌های Coq تعبیه‌شده در فایل‌های LaTeX
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coq\-tex
[
.BI \-o \ output-file
]
[
.BI \-n \ line-width
]
[
.BI \-image \ coq-image
]
[
.B \-w
]
[
.B \-v
]
[
.B \-sl
]
[
.B \-hrule
]
[
.B \-small
]
.I input-file .\|.\|.
.
.
.SH "توضیحات (DESCRIPTION)"
.
فیلتر
.B coq\-tex
عبارت‌های Coq تعبیه‌شده در فایل‌های LaTeX را استخراج و ارزیابی کرده و نتیجهٔ ارزیابی را پس از هر عبارت درج می‌کند.
.PP
سه محیط LaTeX برای گنجاندن کد Coq در فایل‌های ورودی فراهم شده است:
.TP
.B coq_example
عبارت‌های میان \\begin{coq_example} و \\end{coq_example} ارزیابی شده و در فایل خروجی کپی می‌شوند.
به دنبال هر عبارت، پاسخ حلقهٔ سطح‌بالا (toplevel loop) درج می‌شود.
.TP
.B coq_example*
عبارت‌های میان \\begin{coq_example*} و \\end{coq_example*} ارزیابی شده و در فایل خروجی کپی می‌شوند.
پاسخ‌های حلقهٔ سطح‌بالا نادیده گرفته می‌شوند.
.TP
.B coq_eval
عبارت‌های میان \\begin{coq_eval} و \\end{coq_eval} به صورت خاموش ارزیابی می‌شوند.
آن‌ها در فایل خروجی کپی نمی‌شوند و پاسخ‌های حلقهٔ سطح‌بالا نادیده گرفته می‌شوند.
.PP
کد LaTeX حاصل در فایل
.IR file \&.v.tex
ذخیره می‌شود، در صورتی که نام فایل ورودی به شکل
.IR file \&.tex
باشد؛ در غیر این صورت نام فایل خروجی همان نام فایل ورودی به همراه پسوند `.v.tex' خواهد بود.
.PP
فایل‌های تولیدشده توسط
.B coq\-tex
می‌توانند مستقیماً توسط LaTeX پردازش شوند.
هم عبارت‌های Coq و هم خروجی حلقهٔ سطح‌بالا با قلم ماشین‌تحریری (typewriter font) حروف‌چینی می‌شوند.
.
.SH "گزینه‌ها (OPTIONS)"
.
.TP
.BI \-o \ output-file
نام فایلی را مشخص می‌کند که خروجی LaTeX باید در آن ذخیره شود.
یک خط تیره `\-' موجب چاپ خروجی LaTeX در خروجی استاندارد می‌شود.
.TP
.BI \-n \ line-width
عرض خط را تعیین می‌کند.
مقدار پیش‌فرض ۷۲ نویسه است.
اگر پاسخ‌های حلقهٔ سطح‌بالا طولانی‌تر از عرض خط باشند، شکسته می‌شوند.
هیچ شکستی روی متن ورودی Coq اعمال نمی‌شود.
.TP
.BI \-image \ coq-image
باعث می‌شود فایل
.I coq-image
برای ارزیابی عبارت‌های Coq اجرا شود.
به طور پیش‌فرض، از دستور
.I coqtop
بدون تعیین هیچ مسیری برای ارزیابی عبارت‌های Coq استفاده می‌شود.
.TP
.B \-w
باعث می‌شود خطوط در صورت امکان روی نویسهٔ فاصله شکسته شوند تا از نصف شدن کلمات در خروجی جلوگیری گردد.
به طور پیش‌فرض، شکستن خطوط بدون توجه به نصف شدن کلمات و در محدودهٔ عرض خط انجام می‌پذیرد.
.TP
.B \-v
حالت پرگو (verbose).
پاسخ‌های Coq را در خروجی استاندارد چاپ می‌کند.
برای تشخیص خطاها در عبارت‌های Coq سودمند است.
.TP
.B \-sl
حالت مایل (slanted).
پاسخ‌های Coq با قلم مایل نوشته می‌شوند.
.TP
.B \-hrule
حالت خطوط افقی.
بخش‌های Coq میان دو خط افقی نوشته می‌شوند.
.TP
.B \-small
حالت قلم کوچک.
بخش‌های Coq با قلمی کوچک‌تر نوشته می‌شوند.
.
.
.SH "هشدارها (CAVEATS)"
عبارت‌های \\begin.\|.\|. و \\end.\|.\|. باید به تنهایی در یک خط قرار گیرند، بدون هیچ نویسه‌ای پیش از بک‌اسلش یا پس از آکولاد بسته.
هر عبارت Coq باید با یک `.' در انتهای خط خاتمه یابد.
وجود فاصلهٔ خالی میان `.' و خط جدید مجاز است، اما هر نویسهٔ دیگر باعث می‌شود که
.B coq\-tex
پایان عبارت را نادیده بگیرد، که این امر به درهم‌ریختگی و عدم تطابق پاسخ‌ها با عبارت‌ها می‌انجامد.
(پاسخ‌ها «عقب می‌افتند».)
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR coqtop (1)