I'm working on a colleague's embedding of modal logic in Coq and I'm trying to define a custom notation for formulas of said logic, like presented here and also on Volume 2 of the book Software Foundations. So far I have this:
Declare Custom Entry modal.
Declare Scope modal_scope.
Notation "[! m !]" := m (at level 0, m custom modal at level 99) : modal_scope.
Notation " p -> q " := (Implies p q) (in custom modal at level 13, right associativity).
Open Scope modal_scope.
Definition test:
[! p -> q !].
However, the Definition gives this error:
Syntax error: [constr:modal level 99] expected after '[!' (in [constr:operconstr]).
And I can't figure out why. I found some questions on SO where the suggested solution is to change the precedence of the first symbol, p in this case, however that just throws another error. The Coq manual wasn't very helpful either.
What is causing this error and why do the other notations work ?
You declared your own syntactic category for your logic: The parser, after [!, expects only things that are in the entry modal. p is an identifier, and the parser does not expect arbitrary identifiers.
In the documentation on custom entries, you can find a hint on how to add identifiers to your entry:
Declare Custom Entry modal.
Declare Scope modal_scope.
Print Grammar constr.
Axiom Implies : Prop -> Prop -> Prop.
Notation "x" := x (in custom modal at level 0, x ident).
Notation "[! m !]" := m (at level 0, m custom modal at level 99) : modal_scope.
Notation "p '->' q" := (Implies p q) (in custom modal at level 13, right associativity).
Open Scope modal_scope.
Definition testp p q:
[! p -> q !] .
I found some questions on SO where the suggested solution is to change the precedence of the first symbol, p in this case, however that just throws another error. The Coq manual wasn't very helpful either.
This can be a solution if the left-most symbol of your notation is a terminal, not a variable.