कोकाइड - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

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 सेवाओं का उपयोग करके ऑनलाइन कोकाइड का उपयोग करें