A bit confused with notations

Using Coq
1

Hi everyone,

I am trying to define some notations for my project but I am a bit confused with how to actually define it.
For the first case, I would like to have the following :

Notation "'on' v { s }" := (Baz v s) : my_scope.

If I try to use it it complains with a Syntax error: [constr:operconstr] expected after [constr:operconstr level 200] (in [constr:operconstr]).. I imagine it might have something to do with this in the docs, but… I don’t know. If I define it like this:

Notation "'on' v { s }" := (Baz v s) (v at next level, s at next level) : my_scope.

Then everything is ok, but I don’t completely understand what is happening (I have an idea but not sure).

The second case is the following:

Notation "f ( a )" := (Bar1 f a) (at level 20) : my_scope.
Notation "l : f ( a )" := (Bar2 l f a) (at level 20) : my_scope.
Notation "f ( a ) { s }" := (Bar3 f a s) (at level 20) : my_scope.
Notation "l : f ( a ) { s }" := (Bar4 l f a s) (at level 20) : my_scope.

If I use any of these in a function I get : Syntax error: '(' expected after [constr:pattern level 200] (in [constr:pattern]).. For instance in the following function:

Definition foo (bar : Bar) := 
    match bar with 
    | _ : _ ( _ ) => true 
    | _ => false 
    end.

And again, I am not entirely sure what to do… I am guessing I have to adjust the levels of the different parameters, but I’m not sure I understand what is happening :laughing:.

Thanks in advance !

2 Likes
2

Actually, with that example function I get :
Error: Such pattern cannot have arguments.

So another one would be :

Definition foo (bar : Bar) := 
    match bar with 
    | l : f ( a ) => true 
    | _ => false 
    end.
3

This seems like a particularly hard problem because all three of _ : _, ( _ ) and { _ } are already used in Coq’s syntax, but I’m also a noob at Coq notations. Custom entries might be worth trying out.

4

Yeah… I know :slightly_frowning_face: .

I’ll take a look at custom entries, thanks !

5

Can you give us a fully (non-)working example? The problem might be hard in general, but maybe it’s solvable for your particular use-case if you show us the actual definitions involved :slight_smile:

1 Like