انگلیسیفرانسویاسپانیایی

Ad


فاویکون OnWorks

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

coqide.byte را در ارائه دهنده هاست رایگان OnWorks از طریق Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا کنید.

این دستور coqide.byte است که می تواند در ارائه دهنده هاست رایگان OnWorks با استفاده از یکی از چندین ایستگاه کاری آنلاین رایگان ما مانند Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا شود.

برنامه:

نام


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 به صورت آنلاین استفاده کنید


سرورها و ایستگاه های کاری رایگان

دانلود برنامه های ویندوز و لینوکس

  • 1
    DivFix ++
    DivFix ++
    DivFix++ مال شما تعمیر ویدئو AVI و
    نرم افزار پیش نمایش برای تعمیر طراحی شده است
    و پیش نمایش فایل هایی که در حال دانلود هستند
    از ed2k(emule)، تورنت، gnutella، ftp...
    DivFix++ را دانلود کنید
  • 2
    انجمن JBoss
    انجمن JBoss
    پروژه های جامعه محور که شامل
    آخرین نوآوری ها برای لبه برش
    برنامه ها پروژه شاخص ما JBoss AS است
    منبع باز پیشرو،
    مطابق با استانداردهای ...
    انجمن JBoss را دانلود کنید
  • 3
    فایلر جنگو
    فایلر جنگو
    django Filer یک مدیریت فایل است
    برنامه ای برای جنگو که می سازد
    دست زدن به فایل ها و تصاویر به سرعت.
    django-filer یک مدیریت فایل است
    برنامه برای djang ...
    دانلود فایل جنگو
  • 4
    xCAT
    xCAT
    مجموعه ابزار مدیریت خوشه افراطی.
    xCAT یک مدیریت خوشه مقیاس پذیر است
    و ابزار تامینی که فراهم می کند
    کنترل سخت افزار، کشف و سیستم عامل
    دیسک پر/دی...
    xCAT را دانلود کنید
  • 5
    PSI
    PSI
    Psi XMPP قدرتمند بین پلتفرمی است
    مشتری برای کاربران با تجربه طراحی شده است.
    بیلدهایی برای ام اس وجود دارد
    ویندوز، گنو/لینوکس و macOS.. مخاطب:
    کاربران نهایی ...
    Psi را دانلود کنید
  • 6
    بلابی والی 2
    بلابی والی 2
    ادامه رسمی معروف
    بازی آرکید Blobby Volley 1.x..
    مخاطب: کاربران نهایی/رومیزی. کاربر
    رابط: OpenGL، SDL. برنامه نويسي
    زبان: C++، Lua. سی...
    دانلود Blobby Volley 2
  • بیشتر "

دستورات لینوکس

Ad