Coq：定义前缀符号

【问题标题】：Coq: Defining a prefix notationCoq：定义前缀符号
【发布时间】：2017-05-13 20:19:52
【问题描述】：

我尝试过使用不同的符号，但无法让我的前缀表示法起作用（另一方面，中缀起作用）。我想这是一个水平问题，但无法解决。有什么想法吗？

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
... *)

【问题讨论】：

标签： parsing syntax symbols coq notation

【解决方案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) *)

【讨论】：