Coq: एक बाएं पुनरावर्ती अंकन एक स्पष्ट स्तर

Question

मैं के लिए एक Coq अंकन परिभाषा देखा है होना चाहिए "का मूल्यांकन करता है करने के लिए" इस प्रकार है:

Notation "e '||' n" := (aevalR e n) : type_scope. 

मैं || के रूप में कुछ और करने के लिए प्रतीक '||' बदलने के लिए कोशिश कर रहा हूँ अक्सर लॉजिकल or के लिए उपयोग किया जाता है। हालांकि, मैं हमेशा एक त्रुटि

A left-recursive notation must have an explicit level 

उदाहरण के लिए मिलता है, ऐसा होता है जब मैं करने के लिए '||' बदलने के लिए:

'\|/', '\||/', '|_|', '|.|', '|v|', या '|_'।

वहाँ कुछ || यहाँ के बारे में खास है? और इन अन्य नोटेशन को काम करने के लिए इसे कैसे ठीक किया जाना चाहिए (यदि संभव हो)?

Answer 1

अगर मैं सही हूँ, यदि आप एक अंकन ओवरलोड, Coq पहले परिभाषा के गुणों का उपयोग करता है। नोटेशन _ '||' _ पहले से ही एक स्तर है, इसलिए Coq आपकी परिभाषा के लिए इस स्तर का उपयोग करता है।

लेकिन नए प्रतीकों के साथ, Coq ऐसा नहीं कर सकते हैं, और आप स्तर निर्दिष्ट करना होगा:

Notation "e '|.|' n" := (aevalR e n) (at level 50) : type_scope. 

पहले से परिभाषित अंकन के लिए, यह क्या मैं ऊपर लिखा था की तुलना में मजबूत है। आप एक नोटेशन के स्तर को फिर से परिभाषित नहीं कर सकते हैं। उदाहरण के लिए प्रयास करें:

Notation "e '||' n" := (aevalR e n) (at level 20) : type_scope.