Coq：接頭辞表記を定義する

Question

私は別の記号で試しましたが、私の接頭辞表記を機能させることはできません（逆に、接尾辞は機能します）。私はそれはレベルの問題だと思いますが、それを並べ替えることはできませんでした。何か案は？

Variable (X R: Type)(x:X)(r:R). 
Variable In: X -> R -> Prop. 
Variable rt:> R -> Type. 
Variable rTr: forall (x:X)(y:R), In x y -> y. 
Notation "' a b" := (rTr a b I) (at level 9). 
(* Check ' x r. -- Syntax error: [constr:operconstr] expected after 
[constr:operconstr level 200] (in [constr:operconstr]). *) 

Notation "a ' b" := (rTr a b I) (at level 9). 
Fail Check x ' r. (* Works (half-compiles) *) 
Print Grammar constr. 
(* ... 
| "9" LEFTA 
    [ SELF; "'"; NEXT 
    | "'"; constr:operconstr LEVEL "200"; NEXT 
... *) 

Answer 1

トリック'のものと少なくとも同程度の低aのレベルを指定することでした。また、両方が10未満でなければならなかった：

Notation "' a b" := (rTr a b I) (at level 9, a at level 9). 
Fail Check ' x r. (* Works (half-compiles) *) 

はまた、接頭表記のabbreviationバージョンは、W /アウト問題（のみ迷惑はシンボルは略語で禁止されていることであるが）仕事：

Notation T a b := (rTr a b I). 
Fail Check T x r. (* Works (half-compiles) *)