Ensembles はより柔軟であるため、今では sで多くの作業を開始しました。それを助けるために、いくつかの便利な表記法を定義しようとしています。たとえば、以下は比較的簡単です。
Notation "a ∈ S" := (@In _ S a) (at level 80).
そして、他の二項集合演算子にも同様の束を追加できます。
しかし、私はこのような表記法で多くの問題を抱えています:
Notation "∀ x ∈ S , P" := (forall x, (x ∈ S) -> P) (at level 90).
受け入れられますが、使用しようとするたびに次のエラーが発生します。
構文エラー: [constr:operconstr レベル 200] ([constr:operconstr] 内) の後に "ε" が必要です。
質問 1:何が間違っていますか?
おまけとして、再帰的な記法を定義する方法を教えてもらえますか? 試してみましたが、まったく新しい一連の問題が発生するようです。ライブラリ定義の簡単な編集である私の試みは次のとおりです。
Notation "∀ x .. y ∈ S , P" :=
(forall x, (x ∈ S) -> .. (forall y, (y ∈ S) -> P) ..)
(at level 200, x binder, y binder, right associativity).
Coq.Unicode.Utf8_coreライブラリのバージョンが解析されるべきで、私のものは解析されるべきではない理由がわかりませんが、
エラー: 再帰パターンの開始位置が見つかりません。
質問 2:質問 1 を参照してください。