coq-tex - آنلاین در ابر

برنامه:

نام

coq-tex - عبارات Coq را پردازش کنید که در فایل های LaTeX تعبیه شده است

خلاصه

coq-tex [ -o فایل خروجی ] [ -n عرض خط ] [ -تصویر تصویر coq ] [ -w ] [ -v ] [ -SL ] [
-هول ] [ -کم اهمیت ] فایل ورودی ...

شرح

La coq-tex فیلتر عبارات Coq تعبیه شده در فایل های LaTeX را استخراج می کند، آنها را ارزیابی می کند و
نتیجه ارزیابی را بعد از هر عبارت درج کنید.

سه محیط LaTeX برای گنجاندن کد Coq در فایل های ورودی ارائه شده است:

coq_example
عبارات بین \begin{coq_example} و \end{coq_example} ارزیابی می‌شوند و
در فایل خروجی کپی شد هر عبارت با پاسخ از
حلقه سطح بالا

coq_example*
عبارات بین \begin{coq_example*} و \end{coq_example*} ارزیابی می‌شوند و
در فایل خروجی کپی شد پاسخ های حلقه سطح بالا کنار گذاشته می شوند.

coq_eval
عبارات بین \begin{coq_eval} و \end{coq_eval} بی‌صدا ارزیابی می‌شوند.
آنها در فایل خروجی و پاسخ های حلقه بالا کپی نمی شوند
دور ریخته می شوند.

کد LaTeX حاصل در فایل ذخیره می شود پروندهاگر فایل ورودی نامی داشته باشد v.tex
فرم پرونده.tex، در غیر این صورت نام فایل خروجی نام فایل ورودی است
با ".v.tex" ضمیمه شده است.

فایل های تولید شده توسط coq-tex می تواند به طور مستقیم توسط LaTeX پردازش شود. هر دو عبارت Coq
و خروجی های سطح بالایی با فونت ماشین تحریر تایپ می شوند.

OPTIONS

-o فایل خروجی
نام فایلی را که قرار است خروجی LaTeX در آن ذخیره شود را مشخص کنید. یک خط تیره «-»
باعث می شود خروجی LaTeX روی خروجی استاندارد چاپ شود.

-n عرض خط
عرض خط را تنظیم کنید. پیش فرض 72 کاراکتر است. پاسخ های سطح بالا
حلقه ها اگر بلندتر از عرض خط باشند تا می شوند. هیچ تاشو روی آن انجام نمی شود
متن ورودی Coq

-تصویر تصویر coq
باعث ایجاد فایل تصویر coq برای ارزیابی عبارات Coq اجرا شود. به صورت پیش فرض،
این دستور است coqtop بدون تعیین مسیری که برای ارزیابی استفاده می شود
عبارات Coq

-w در صورت امکان، خطوط را روی یک کاراکتر فاصله تا کنید و از برش کلمات اجتناب کنید
در خروجی به‌طور پیش‌فرض، بدون توجه به کلمه، تا کردن در عرض خط رخ می‌دهد
برش ها

-v حالت پرمخاطب. پاسخ های Coq را روی خروجی استاندارد چاپ می کند. برای تشخیص مفید است
اشتباهات در عبارات Coq

-SL حالت کج. پاسخ های Coq با فونت اریب نوشته شده است.

-هول حالت خطوط افقی قسمت های Coq بین دو خط افقی نوشته می شوند.

-کم اهمیت حالت فونت کوچک قسمت های Coq با فونت کوچکتر نوشته شده اند.

هشدارها

عبارات \ آغاز ... و \ پایان ... باید بدون هیچ کاراکتری روی یک خط قرار گیرند
قبل از بک اسلش یا بعد از بستن بریس. هر عبارت Coq باید توسط
'.' در انتهای یک خط فضای خالی بین «.» پذیرفته می شود. و خط جدید، اما هر
کاراکتر دیگر باعث می شود که coq-tex انتهای عبارت را نادیده بگیرد و در نتیجه یک
درهم ریختن نادرست پاسخ ها در عبارات. (پاسخ‌ها «عقب مانده‌اند».)

با استفاده از خدمات onworks.net از coq-tex به صورت آنلاین استفاده کنید