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/out 个问题（唯一的烦恼是缩写中禁止使用符号）：

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

Coq：定义前缀符号

Coq: Defining a prefix notation

syntax

parsing

symbols

notation

coq