coq-tex - عبر الإنترنت في السحابة

برنامج:

اسم

coq-tex - معالجة عبارات Coq المضمنة في ملفات LaTeX

موجز

كوك-تكس [ -o ملف إلاخراج ] [ -n عرض الخط ] [ -صورة صورة coq ] [ -w ] [ -v ] [ -سل ] [
-حرول ] [ -صغير ] ملف الإدخال

الوصف

• كوك-تكس يقوم عامل التصفية باستخراج عبارات Coq المضمنة في ملفات LaTeX وتقييمها و
أدخل نتيجة التقييم بعد كل عبارة.

يتم توفير ثلاث بيئات LaTeX لتضمين كود Coq في ملفات الإدخال:

مثال_ق
العبارات الواقعة بين \ begin {coq_example} و \ end {coq_example} يتم تقييمها و
نسخها في ملف الإخراج. كل عبارة تليها استجابة
حلقة toplevel.

مثال_ coq *
يتم تقييم العبارات بين \ begin {coq_example *} و \ end {coq_example *} و
نسخها في ملف الإخراج. يتم تجاهل استجابات الحلقة toplevel.

coq_eval
يتم تقييم العبارات الواقعة بين \ begin {coq_eval} و \ end {coq_eval} بصمت.
لا يتم نسخها في ملف الإخراج ، واستجابات حلقة toplevel
يتم التخلص منها.

يتم تخزين كود LaTeX الناتج في الملف ملف.v.tex إذا كان لملف الإدخال اسم
الاستمارة ملف.tex ، وإلا فإن اسم ملف الإخراج هو اسم ملف الإدخال
مع ملحق ".v.tex".

الملفات التي تم إنتاجها بواسطة كوك-تكس يمكن معالجتها مباشرة بواسطة LaTeX. كل من عبارات Coq
ويتم تعيين الإخراج toplevel بخط الآلة الكاتبة.

OPTIONS

-o ملف إلاخراج
حدد اسم الملف الذي سيتم تخزين ناتج LaTeX فيه. اندفاعة "-"
يؤدي إلى طباعة إخراج LaTeX على الإخراج القياسي.

-n عرض الخط
اضبط عرض الخط. الافتراضي هو 72 حرفًا. ردود toplevel
يتم طي الحلقة إذا كانت أطول من عرض الخط. لا يتم إجراء الطي على
نص إدخال Coq.

-صورة صورة coq
تسبب الملف صورة coq ليتم تنفيذها لتقييم عبارات Coq. بشكل افتراضي،
هذا هو الأمر com.coqtop بدون تحديد أي مسار يتم استخدامه للتقييم
عبارات Coq.

-w تسبب في طي السطور على حرف مسافة كلما أمكن ذلك ، وتجنب قطع الكلمات
في الإخراج. بشكل افتراضي ، يحدث الطي عند عرض الخط ، بغض النظر عن الكلمة
يقطع.

-v وضع مفصل. يطبع إجابات Coq على الإخراج القياسي. مفيد للكشف
أخطاء في عبارات Coq.

-سل الوضع المائل. تتم كتابة إجابات Coq بخط مائل.

-حرول وضع الخطوط الأفقية. تتم كتابة أجزاء Coq بين سطرين أفقيين.

-صغير وضع الخط الصغير. تمت كتابة أجزاء Coq بخط أصغر.

تحفظات

يجب أن توضع العبارات \ start ... and end ... على سطر بمفردها ، بدون أحرف
قبل الخط المائل العكسي أو بعد قوس الإغلاق. يجب إنهاء كل عبارة Coq بواسطة
"." في نهاية السطر. يتم قبول مسافة فارغة بين "." والخط الجديد ، ولكن أي
سيؤدي الحرف الآخر إلى تجاهل coq-tex لنهاية العبارة ، مما يؤدي إلى ظهور ملف
خلط الردود بشكل غير صحيح في العبارات. (الردود `` متخلفة ".)

استخدم coq-tex عبر الإنترنت باستخدام خدمات onworks.net