2012-11-29 15 views
6

अन्य लेखकों के कोक सबूत का अध्ययन करने में, मुझे अक्सर एक रणनीति का सामना करना पड़ता है, "आइक्क हेक" या "intro_b" कहें। मैं ऐसी रणनीति को समझना चाहता हूं।कोक सबूत में एक रणनीति की परिभाषा की परिभाषा

मुझे कैसे पता चलेगा कि यह एक कॉक रणनीति है या मेरी वर्तमान परियोजना में कहीं भी एक रणनीति नोटेशन परिभाषित किया गया है?

दूसरा, क्या इसकी परिभाषा को खोजने का कोई तरीका है?

मैंने खोजअबाउट, खोज, पता लगाएँ और प्रिंट का उपयोग किया लेकिन उपरोक्त प्रश्नों के उत्तर नहीं मिल सके।

उत्तर

4

आप

Print Ltac <tacticname>. 

उपयोग करने के लिए एक उपयोगकर्ता-निर्धारित रणनीति के कोड मुद्रित करने के लिए (documentation के अनुसार) सक्षम होना चाहिए।


जहां यह परिभाषित किया गया है ... मुझे लगता है कि आप ग्रेप जरूरत के लिए दुर्भाग्य से, Locate रणनीति नाम ऐसा लगता है के लिए काम नहीं करता जा रहे हैं पता करने के लिए।

+1

'पता लगाएँ Ltac'' Locate' –

2

जैसा कि पहले बताया गया है, Print Ltac ... उपयोगकर्ता द्वारा परिभाषित रणनीति के कोड को मुद्रित करता है।

उपयोगकर्ता द्वारा परिभाषित रणनीति का पता लगाने के लिए (यानी यह जानना कि इसकी परिभाषा कहां है), Locate Ltac ... का उपयोग करें। यह आपको पूरी तरह से योग्य नाम देता है। फिर संबंधित फ़ाइल को खोजने के लिए Locate Library का उपयोग करें।

+0

@ स्पेसबीयर का सामरिक संस्करण है: मुझे लगता है कि आप बस उलझन में हैं। यह एक उत्तर है, किसी भी तरह से आलोचना या स्पष्टीकरण के लिए अनुरोध नहीं है। –

+0

हां पूरी तरह से। गलत बटन दबाएं। टिप्पणी हटा दी गई। – SpaceBeers

+0

@downvoter, कृपया एक टिप्पणी छोड़ दो? –