Coq：定义前缀记法

Question

我试过w /不同的符号，但不能让我的前缀表示法工作（中缀，另一方面，作品）。我想这是一个级别的问题，但无法整理出来。有任何想法吗？

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版本的前缀符号的工作瓦特/出的问题（唯一的烦恼在于符号的缩写禁止）：

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