coqmktop - מקוון בענן

תָכְנִית:

שֵׁם

coqmktop - מקשר טקטיקת משתמש Coq Proof Assistant

תַקצִיר

coqmktop [ אפשרויות ] קבצים

תיאור

coqmktop בונה רמת Coq חדשה מורחבת עם טקטיקות משתמש. קבצים הם המטרה
קבצי אובייקט או ספריה של Caml (כלומר עם הסיומת .cmo, .cmx, .cma או .cmxa) לקישור עם
מערכת Coq. המקשר מייצר Coq toplevel שניתן להפעיל אותו ניתן לקרוא ישירות
או דרך coqc(1), באמצעות האפשרות -image.

אפשרויות

-h עֶזרָה. רשום את האפשרויות הזמינות.

-srcdir dir
ציין היכן נמצאים קבצי המקור של Coq

-o קובץ exec
ציין את שם הרמה העליונה שהתקבלה

-העדיף קומפילציה בקוד מקורי

-מלא קישור טקטיקות ברמה גבוהה

-חלק עליון בנה Coq על רמה עליון של ocaml (לא תואם עם -העדיף)

-R dir ציין ספריות רקורסיביות עבור Ocaml

-v8 קישור לדקדוק V8

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