कॉकटॉप - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

कॉकटॉप - कॉक प्रूफ असिस्टेंट टॉपलेवल सिस्टम

SYNOPSIS

कोकटॉप [ विकल्पों ]

वर्णन

कोकटॉप इंटरैक्टिव उपयोग के लिए Coq की शीर्ष स्तरीय प्रणाली है। यह पर वाक्यांश पढ़ता है
मानक इनपुट, और मानक आउटपुट पर परिणाम प्रिंट करता है।

Coq के बैच-उन्मुख उपयोग के लिए, देखें सीओक्यूसी(1).

विकल्प

-एच, --मदद
मदद करना। आपको coqtop द्वारा स्वीकृत विकल्पों की पूरी सूची देगा।

-I डीआईआर, --शामिल दीर
निर्देशिका जोड़ें दीर शामिल पथ में

-R दीर कोकदिर
भौतिक रूप से पुनरावर्ती मानचित्रण करें दीर तार्किक करने के लिए कोकदिर

-top कोकदिर
शीर्ष स्तर का नाम सेट करें कोकदिर शीर्ष के बजाय

-इनपुट स्थिति फ़ाइल का नाम, -है फ़ाइल का नाम
फ़ाइल से स्थिति पढ़ें फ़ाइलनाम.coq

-नोइस एक खाली प्रारंभिक स्थिति से प्रारंभ करें

-आउटपुटस्टेटफ़ाइल का नाम
फ़ाइल में स्थिति लिखें फ़ाइलनाम.coq

-लोड-एमएल-ऑब्जेक्ट फ़ाइल का नाम
एमएल ऑब्जेक्ट फ़ाइल लोड करें फ़ाइलनाम

-लोड-एमएल-स्रोत फ़ाइल का नाम
एमएल फ़ाइल लोड करें फ़ाइल का नाम

-लोड-वर्नाक-स्रोत फ़ाइल का नाम, -l फ़ाइल का नाम
Coq फ़ाइल लोड करें फ़ाइल नाम.v (फ़ाइल नाम लोड करें।)

-लोड-वर्नाक-स्रोत-वर्बोज़ फ़ाइल का नाम, -एलवी फ़ाइल का नाम
वर्बोज़ली Coq फ़ाइल लोड करें फ़ाइल नाम.v (वर्बोज़ फ़ाइल नाम लोड करें।)

-लोड-वर्नैक-ऑब्जेक्ट फ़ाइल का नाम
Coq ऑब्जेक्ट फ़ाइल लोड करें फ़ाइलनाम.vo

-आवश्यकता फ़ाइल का नाम
Coq ऑब्जेक्ट फ़ाइल लोड करें फ़ाइलनाम.vo और इसे आयात करें (फ़ाइल नाम आयात की आवश्यकता है।)

-संकलित फ़ाइल का नाम
Coq फ़ाइल संकलित करें फ़ाइल नाम.v (तात्पर्य -बैच )

-संकलन-क्रिया फ़ाइल का नाम
Coq फ़ाइल को शब्दशः संकलित करें फ़ाइल नाम.v (तात्पर्य -बैच )

-आय Coq का मूल-कोड संस्करण चलाएँ

-बाइट Coq का बाइटकोड संस्करण चलाएँ

-कहां है Coq के मानक पुस्तकालय स्थान और निकास को प्रिंट करें

-v Coq संस्करण प्रिंट करें और बाहर निकलें

-q rcfile की लोडिंग छोड़ें

-इनिट-फाइल फ़ाइल का नाम
आरसीफ़ाइल को सेट करें फ़ाइल का नाम

-बैच बैच मोड (तर्क पार्सिंग के ठीक बाद बाहर निकलता है)

-बूट बूट मोड (मतलब -q और -बैच )

-emacs Coq को बताता है कि इसे Emacs के अंतर्गत निष्पादित किया जाता है

-डंप-ग्लोब फ़ाइल का नाम
फ़ाइल f में वैश्वीकरण को डंप करें (द्वारा उपयोग किया जाएगा)। कोकडॉक(1) )

-जियोप्रूफ के साथ (हाँ|नहीं)
(डी) कोकाइड के भीतर जियोप्रूफ़ के लिए विशेष कार्यों को सक्रिय करना (डिफ़ॉल्ट है)। हाँ )

-अप्रत्याशित-सेट
सेट सॉर्ट सेट अप्रेडिकेटिव

-न-लोड-सबूत
स्मृति में अपारदर्शी प्रमाण लोड न करें

-एक्सएमएल XML फ़ाइलों को या तो निर्देशिका में निहित पदानुक्रम में निर्यात करें
$COQ_XML_LIBRARY_ROOT (यदि सेट है) या stdout करने के लिए (यदि सेट नहीं है)

गुणवत्ता
कुछ युक्तियों द्वारा उत्पादित प्रमाण शब्दों की सुपाठ्यता में सुधार करें

onworks.net सेवाओं का उपयोग करके ऑनलाइन coqtop का उपयोग करें