गैलिना - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

गैलिना - Coq स्थानीय फ़ाइलों से विशिष्टताएँ निकालता है

SYNOPSIS

मुर्गी [ - ] [ -स्टडआउट ] [ -कोई टिप्पणी नहीं ] पट्टिका ...

वर्णन

मुर्गी Coq फ़ाइलों को तर्क के रूप में लेता है और संबंधित विनिर्देश फ़ाइलें बनाता है।
Coq फ़ाइल foo.v विशिष्टता फ़ाइल को जन्म देता है foo.g. प्रत्यय '.जी' खड़ा है
गैलिना के लिए.

उस उद्देश्य के लिए, गैलिना उन सभी आदेशों को हटा देती है जो "प्रमेय", "लेम्मा", "तथ्य" का पालन करते हैं।
"टिप्पणी" या "लक्ष्य" कथन जब तक कि यह "निरस्त करें", "सहेजें", "प्रश्न" आदेश तक न पहुंच जाए।
"परिभाषित।" या "प्रमाण <...>।" यह प्रत्येक "संकेत", "वाक्यविन्यास", "तत्काल" या को भी हटा देता है
"पारदर्शी" आदेश.

.v प्रत्यय के बिना फ़ाइलों को नजरअंदाज कर दिया जाता है।

विकल्प

-स्टडआउट
परिणाम को मानक आउटपुट पर प्रिंट करता है।

- Coq स्रोत मानक इनपुट पर लिया गया है। परिणाम मानक आउटपुट पर मुद्रित होता है।

-कोई टिप्पणी नहीं
टिप्पणियाँ *.g फ़ाइल में हटा दी जाती हैं।

टिप्पणियाँ

नेस्टेड टिप्पणियाँ सही ढंग से प्रबंधित की जाती हैं। विशेष रूप से, प्रत्येक आदेश "सहेजें।" या "निरस्त करें।" में
किसी टिप्पणी पर ध्यान नहीं दिया जाता.

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