のCoQ：</p> <pre><code>Notation "e '||' n" := (aevalR e n) : type_scope. </code></pre> <p>を私は<code>||</code>として何か他にシンボル<code>'||'</code>を変更しようとしています：左再帰的な表記法は、私は次のように「と評価さ」のためのCoqの表記の定義を見てきました明示的なレベル

Question

を持っている必要があります論理orにはしばしば使用されます。

'\|/'、'\||/'、'|_|'、'|.|'、'|v|'、または'|_'：しかし、私は常に例えばエラー

A left-recursive notation must have an explicit level 

を得る私は'||'を変更すると、これは起こります。

||には特別なものがありますか？これらの他の表記法を可能にするためにはどうすればよいでしょうか？

Answer 1

私が正しいとすれば、Coqは表記法をオーバーロードすると、最初の定義のプロパティを使用します。 _ '||' _という表記はすでにレベルがあるため、Coqはこのレベルを定義に使用します。

しかし、新しいシンボルで、コックはそれを行うことができない、とあなたがレベルを指定する必要があります。すでに定義されて表記については

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

、これは私が上で書いたものよりもさらに強力です。表記法のレベルを再定義することはできません。たとえば、次のように試してみてください：

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