1
我試過w /不同的符號,但不能讓我的前綴表示法工作(中綴,另一方面,作品)。我想這是一個級別的問題,但無法整理出來。有任何想法嗎?Coq:定義前綴記法
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
... *)