Coq: Defining a prefix notation

Question

I've tried w/ different symbols but cannot get my prefix notation to work (infix, on the other hand, works). I guess it's a level problem but couldn't sort it out. Any ideas?

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

jaam jaam · Accepted Answer · 2017-05-25T16:18:10

The trick was to specify a's level at least as low as that of '. Also, both had to be less than 10:

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

Also, the abbreviation version of the prefix notation worked w/out problems (the only annoyance being that symbols are barred in abbreviations):

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

Coq: Defining a prefix notation

1 Answers