長いdistfixをいじるために、自分のスコープが欲しいです。
Declare Scope my_scope.
Delimit Scope my_scope with my.
Open Scope my_scope.
Definition f (x y a b : nat) : nat := x+y+a+b.
Notation "x < y * a = b" := (f x y a b)
(at level 100, no associativity) : my_scope.
Check (1 < 2 * 3 = 4)%my.
新しいスコープをどのように作成しますか?
編集：「x < y * a = b」を選択して、Coqの演算子をオーバーライドしました（それぞれ優先順位が異なります）。
コマンドDeclare Scopeが存在しません。スコープに関するさまざまなコマンドは、Coq マニュアルのセクション 12.2 で説明されています。
表記例の選択には固有の問題があります。それは、表記法の前に使用されているように見える事前定義された表記法と衝突するためです。
パーサーは最初のコンポーネントを見て、_ < _ 実際に整数の比較について話していると判断し、2 番目の部分を記法 のインスタンス_ * _と見なし、それがすべて等式の左辺であると見なします。そして、パーサーは常に満足しており、次の形式の式を構築します。
(1 < (2 * 3)) = 4
これはパーサーによって構築され、型システムはまだ要求されていません。型チェッカーは、自然数を の最初の子と見なし、(_ < _)満足しています。それは(_ * _)2 番目の子であると認識して満足しています。その製品の最初の子が nat 番号であることを認識し、まだ満足しています。最終的には等価であり、この等価の最初のコンポーネントは typePropにありますが、2 番目のコンポーネントは type にありnatます。
回答を入力Locate "_ < _ * _ = _".すると、新しい表記法を定義したことがわかります。問題は、パーサーが以前に使用できる別の表記法を常に見つけるため、この表記法が使用されないことです。Coq のマニュアルの第 12 章の次の文で示唆されているように、ある表記法が別の表記法よりも好まれる理由を理解するには、構文解析技術の知識が必要です (私にはわかりません)。
Coq の拡張可能な解析は、基本的に LL1 パーサーである Camlp5 によって実行されます。
x、 、y、aなどのさまざまな変数のレベルを選択してb、これらの変数のいずれもテキストの大部分と一致しないようにする必要があります。たとえば、私はあなたのものに近い記法を定義しようとしましたが、開始ブラケットと終了ブラケットを使用しました (そして、これによりタスクが大幅に簡素化されると思います)。
Notation "<< x < y * a = b >>" := (f x y a b)
(x at level 59, y at level 39, a at level 59) : my_scope.
のレベルは のレベルxよりも低くなるように=選択され、y のレベルは のレベルよりも低くなるように選択され、*のレベルはaよりも低くなるように選択されます=。レベルはコマンドの答えを読んで取得しましPrint Grammar constr. た。
Check << 1 < 2 * 3 = 4 >>.
しかし、本当に良い記譜法を得るには、もう少しエンジニアリングを含める必要があるかもしれません。