क्या कोक में एक विशिष्ट नोटेशन को अक्षम करने का कोई तरीका है?

Question

मैं चाहता हूं कि, कोक्साइड में, सबूत राज्य एक निश्चित नोटेशन का उपयोग न करें (लेकिन फिर भी अन्य सभी का उपयोग करें)।

क्या यह संभव है?

Answer 1

जो मैं दस्तावेज़ में समझता हूं उससे, यह संभव नहीं है। आप ओपनिंग/क्लोजिंग स्कोप्स के साथ खेलने में सक्षम हो सकते हैं, लेकिन मुझे यकीन नहीं है कि यह काम करेगा, क्योंकि यह स्पष्ट रूप से कहा गया है कि जब भी संभव हो प्रिंटिंग के लिए नोटेशन का उपयोग किया जाएगा।

Answer 2

कुछ चाल है कि पर्याप्त हो सकता है का वर्णन यहां: How to disable my custom notation in Coq?

मुझे लगता है कि जवाब देने के लिए सूचक को जोड़ने के लिए है, क्योंकि इस सवाल का गूगल पर पहले आता है चाहता था।