यह कमांड coqide.byte है जिसे हमारे कई मुफ्त ऑनलाइन वर्कस्टेशन जैसे कि उबंटू ऑनलाइन, फेडोरा ऑनलाइन, विंडोज ऑनलाइन एमुलेटर या मैक ओएस ऑनलाइन एमुलेटर का उपयोग करके ऑनवर्क्स फ्री होस्टिंग प्रदाता में चलाया जा सकता है।
कार्यक्रम:
नाम
coqide - Coq प्रूफ असिस्टेंट ग्राफिकल इंटरफेस
SYNOPSIS
कोकाइड [ विकल्पों ]
वर्णन
कोकाइड Coq प्रूफ असिस्टेंट के लिए gtk ग्राफिकल इंटरफेस है।
Coq के कमांड-लाइन-ओरिएंटेड उपयोग के लिए, देखें कोकटॉप(1) ; Coq के बैच-उन्मुख उपयोग के लिए, देखें
सीओक्यूसी(1).
विकल्प
-h द्वारा स्वीकृत विकल्पों की पूरी सूची दिखाएं कोकाइड.
-I दीर, -शामिल दीर
शामिल पथ में निर्देशिका dir जोड़ें।
-R दीर कोकदिर
पुनरावर्ती रूप से भौतिक मानचित्र करें दीर तार्किक करने के लिए कोकदिर.
-एसआरसी शामिल पथ में स्रोत निर्देशिका जोड़ें।
-है f, -इनपुट स्थिति f
राज्य से पढ़ें f.कोक।
-नोइस एक खाली स्थिति से शुरू करें।
-आउटपुटस्टेट f
फ़ाइल में राज्य लिखें f.कोक।
-लोड-एमएल-ऑब्जेक्ट f
ML ऑब्जेक्ट फ़ाइल लोड करें f.
-लोड-एमएल-स्रोत f
एमएल फ़ाइल लोड करें f.
-l f, -लोड-वर्नाक-स्रोत f
Coq फ़ाइल लोड करें f.v (लोड f।)।
-एलवी f, -लोड-वर्नाक-स्रोत-वर्बोज़ f
Coq फ़ाइल लोड करें f.v (लोड वर्बोज़ f।)।
-लोड-वर्नैक-ऑब्जेक्ट f
Coq ऑब्जेक्ट फ़ाइल लोड करें fवीओ
-आवश्यकता f
Coq ऑब्जेक्ट फ़ाइल लोड करें f.vo और इसे आयात करें (आवश्यकता f।)।
-संकलित f
Coq फ़ाइल संकलित करें f.v (अर्थात् -बैच).
-संकलन-क्रिया f
Coq फ़ाइल को मौखिक रूप से संकलित करें f.v (अर्थात् -बैच).
-आय Coq या Coq_SearchIsos का मूल-कोड संस्करण चलाएँ।
-बाइट Coq या Coq_SearchIsos का बाइटकोड संस्करण चलाएँ।
-कहां है Coq के मानक पुस्तकालय स्थान को प्रिंट करें और बाहर निकलें।
-v Coq संस्करण प्रिंट करें और बाहर निकलें।
-q आरसीफाइल लोड करना छोड़ें।
-इनिट-फाइल f
आरसीफाइल को इस पर सेट करें f.
-बैच बैच मोड (तर्कों को पार्स करने के ठीक बाद बाहर निकलता है)।
-बूट बूट मोड (मतलब -q और -बैच).
-emacs Coq को बताता है कि इसे Emacs के तहत निष्पादित किया जाता है।
-डंप-ग्लोब f
फ़ाइल में डंप वैश्वीकरण f (द्वारा इस्तेमाल किया जाना कोकडॉक(1))।
-अप्रत्याशित-सेट
सॉर्ट सेट करें इंप्रेडिकेटिव सेट करें।
-न-लोड-सबूत
स्मृति में अपारदर्शी प्रमाण लोड न करें।
-एक्सएमएल XML फ़ाइलों को या तो निर्देशिका में निहित पदानुक्रम में निर्यात करें
COQ_XML_LIBRARY_ROOT (यदि सेट हो) या स्टडआउट करने के लिए (यदि सेट न हो)।
onworks.net सेवाओं का उपयोग करके ऑनलाइन coqide.byte का उपयोग करें
