# A bit confused with notations

**URL:** <https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374>\
**Category:** Using Rocq\
**Created:** [August 1, 2019, 8:26pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374 "2019-08-01T20:26:58Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![TDiazT](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tdiazt/32/196_2.png) [@TDiazT](https://discourse.rocq-prover.org/u/TDiazT)\
**Post date:** [August 1, 2019, 8:26pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374/1 "2019-08-01T20:26:58Z")

</div>

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 :

```auto
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](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules), but… I don’t know. If I define it like this:

```auto
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:

```auto
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:

```auto
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 😆.

Thanks in advance !

---

<div class="post-metadata">

**Author:** ![TDiazT](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tdiazt/32/196_2.png) [@TDiazT](https://discourse.rocq-prover.org/u/TDiazT)\
**Post date:** [August 1, 2019, 8:31pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374/2 "2019-08-01T20:31:48Z")

</div>

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

So another one would be :

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

```

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [August 4, 2019, 6:30pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374/3 "2019-08-04T18:30:59Z")

</div>

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](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#custom-entries) might be worth trying out.

---

<div class="post-metadata">

**Author:** ![TDiazT](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tdiazt/32/196_2.png) [@TDiazT](https://discourse.rocq-prover.org/u/TDiazT)\
**Post date:** [August 5, 2019, 2:22pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374/4 "2019-08-05T14:22:15Z")

</div>

Yeah… I know 🙁 .

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

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [August 5, 2019, 3:07pm UTC](https://discourse.rocq-prover.org/t/a-bit-confused-with-notations/374/5 "2019-08-05T15:07:09Z")

</div>

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 🙂