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

برنامج:

اسم

غالينا - يستخرج المواصفات من ملفات Coq العامية

موجز

دجاجة [ - ] [ -المعتاد ] [ -بدون تعليقات ] ملف

الوصف

دجاجة يأخذ ملفات Coq كوسيطات ويبني ملفات المواصفات المقابلة.
ملف كوك foo.v يعطي تفاصيل لملف المواصفات foo.g. اللاحقة ".g" تقف
لغالينا.

لهذا الغرض، تقوم غالينا بإزالة كافة الأوامر التي تتبع "النظرية"، "Lemma"، "الحقيقة"،
عبارة "ملاحظة" أو "الهدف" حتى تصل إلى أمر "إحباط". أو "حفظ". أو "Qed."،
"مُعرف." أو "الدليل <...>.". كما أنه يزيل كل "تلميح" أو "بناء جملة" أو "فوري" أو "
أمر "شفاف".

يتم تجاهل الملفات التي لا تحتوي على اللاحقة ‎.v.

OPTIONS

-المعتاد
طباعة النتيجة على الإخراج القياسي.

- يتم أخذ مصدر Coq على الإدخال القياسي. تتم طباعة النتيجة على الإخراج القياسي.

-بدون تعليقات
تتم إزالة التعليقات في ملف *.g.

الملاحظات

تتم معالجة التعليقات المتداخلة بشكل صحيح. على وجه الخصوص، كل أمر "حفظ". أو "إحباط". في
لا يؤخذ التعليق بعين الاعتبار.

استخدم Gallina عبر الإنترنت باستخدام خدمات onworks.net