coqide.byte - آنلاین در ابر

برنامه:

نام

coqide - رابط گرافیکی Coq Proof Assistant

خلاصه

coqide [ گزینه های ]

شرح

coqide یک رابط گرافیکی gtk برای دستیار اثبات Coq است.

برای استفاده خط فرمان از Coq، نگاه کنید به coqtop(1)؛ برای استفاده دسته‌ای از Coq، نگاه کنید به
coqc(1).

OPTIONS

-h نمایش لیست کامل گزینه های پذیرفته شده توسط coqide.

-I دیر, -عبارتند از دیر
دایرکتوری dir را در مسیر include اضافه کنید.

-R دیر coqdir
نقشه فیزیکی بازگشتی دیر به منطقی coqdir.

-src دایرکتوری های منبع را در مسیر include اضافه کنید.

-است f, -inputstate f
خواندن حالت از f.coq.

-صدا با یک حالت خالی شروع کنید.

-خروجی f
حالت را در فایل بنویسید f.coq.

-load-ml-object f
فایل شی ML را بارگیری کنید f.

منبع -load-ml f
فایل ML را بارگیری کنید f.

-l f, -load-vernac-source f
فایل Coq را بارگیری کنید f.v (بارگیری f).

-lv f, -load-vernac-source-verbose f
فایل Coq را بارگیری کنید f.v (بارگذاری کامل f).

-load-vernac-object f
فایل شی Coq را بارگیری کنید fvo.

-نیاز f
فایل شی Coq را بارگیری کنید f.vo و وارد کنید (نیاز f).

-گردآوری f
فایل Coq را کامپایل کنید f.v (نشان می دهد - دسته ای).

-کامپایل-کلام f
فایل Coq را بطور کامل کامپایل کنید f.v (نشان می دهد - دسته ای).

-بهترین نسخه بومی کد Coq یا Coq_SearchIsos را اجرا کنید.

-بایت نسخه بایت کد Coq یا Coq_SearchIsos را اجرا کنید.

-جایی که چاپ محل کتابخانه استاندارد Coq و خروج.

-v نسخه Coq را چاپ کنید و از آن خارج شوید.

-q از بارگذاری rcfile صرفنظر کنید.

-init-file f
فایل rc را تنظیم کنید f.

- دسته ای حالت دسته ای (درست پس از تجزیه آرگومان ها خارج می شود).

-برو حالت بوت (به معنی -q و - دسته ای).

-امکس به Coq می گوید که تحت Emacs اجرا می شود.

دامپ-گلوب f
جهانی سازی ها را در پرونده بیاندازید f (برای استفاده coqdoc(1).

-مجموعه-محتمل
تنظیم مرتب سازی مجموعه impredicative.

ضد بارگذاری
اثبات های مات را در حافظه بارگذاری نکنید.

-xml فایل های XML را به سلسله مراتبی که در دایرکتوری ریشه دارند صادر کنید
COQ_XML_LIBRARY_ROOT (در صورت تنظیم) یا به stdout (اگر تنظیم نشده باشد).

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