coqtop - מקוון בענן

תָכְנִית:

שֵׁם

coqtop - מערכת Coq Proof Assistant ברמה העליונה

תַקצִיר

coqtop [ אפשרויות ]

תיאור

coqtop היא המערכת העליונה של Coq, לשימוש אינטראקטיבי. זה קורא ביטויים על
קלט סטנדרטי, ומדפיס תוצאות על הפלט הסטנדרטי.

לשימוש מונחה אצווה ב-Coq, ראה coqc(1).

אפשרויות

-ח, - עזרה
עֶזרָה. ייתן לך את הרשימה המלאה של האפשרויות המקובלות על ידי coqtop.

-I דיר, --לִכלוֹל dir
הוסף ספרייה dir בנתיב הכלול

-R dir coqdir
ממפה פיזית רקורסיבית dir להגיוני coqdir

-חלק עליון coqdir
הגדר את השם ברמה העליונה להיות coqdir במקום Top

-מצב קלט שם קובץ, -זה שם הקובץ
קרא מצב מהקובץ filename.coq

-רעש להתחיל עם מצב התחלתי ריק

-מצב פלטשם הקובץ
כתוב מצב בקובץ filename.coq

-load-ml-object שם הקובץ
טען קובץ אובייקט ML שם הקובץ

-load-ml-source שם הקובץ
טען קובץ ML שם הקובץ

-load-vernac-source שם קובץ, -l שם הקובץ
טען קובץ Coq שם קובץ.v (טען את שם הקובץ.)

-load-vernac-source-verbose שם קובץ, -lv שם הקובץ
טען באופן מילולי קובץ Coq שם קובץ.v (טען את שם הקובץ המדויק.)

-load-vernac-object שם הקובץ
טען קובץ אובייקט Coq filename.vo

-לִדרוֹשׁ שם הקובץ
טען קובץ אובייקט Coq filename.vo וייבא אותו (דרוש ייבוא ​​שם קובץ.)

-לְלַקֵט שם הקובץ
קומפיל את קובץ Coq שם קובץ.v (מרמז -קבוצה )

-compile-verbose שם הקובץ
הידור מילולי של קובץ Coq שם קובץ.v (מרמז -קבוצה )

-העדיף הפעל את גרסת הקוד המקורי של Coq

-בייט הפעל את גרסת ה-bytecode של Coq

-איפה הדפס מיקום ויציאה מהספרייה הסטנדרטית של Coq

-v הדפס גרסת Coq ויציאה

-q דלג על טעינת rcfile

-init-file שם הקובץ
הגדר את rcfile ל שם הקובץ

-קבוצה מצב אצווה (יוצא מיד לאחר ניתוח ארגומנטים)

-מַגָף מצב אתחול (מרמז -q ו -קבוצה )

-emacs אומר ל-Coq שזה מבוצע תחת Emacs

-מזבלה-גלוב שם הקובץ
dump גלובליזציות בקובץ f (לשימוש על ידי coqdoc(1) )

-עם-geoproof (כן|לא)
כדי (לבטל) הפעלה של פונקציות מיוחדות עבור Geoproof בתוך Coqide (ברירת המחדל היא כן )

-סט אימפריקטיבי
קבע מיון קבע מאפיין

-אל תעמיס הוכחות
אל תטען הוכחות אטומות בזיכרון

-xml ייצא קובצי XML אל ההיררכיה המושרשת בספריה
$COQ_XML_LIBRARY_ROOT (אם מוגדר) או ל-stdout (אם לא מוגדר)

איכות
לשפר את קריאות מונחי ההוכחה המיוצרים על ידי טקטיקות מסוימות

השתמש ב-coqtop באינטרנט באמצעות שירותי onworks.net