## Stream: Coq users

### Topic: Problem with right associative recursive notation

#### MackieLoeffel (Jun 12 2023 at 06:41):

Hi,
I am trying to build a right associative recursive notation, but I get error messages that I don't understand.
In particular, I would like to define the `andr:` notation from below, but I get an error (see below), while the left associative notation works. Any ideas what is going on and how to fix this?

``````Notation "'andr:' | x | .. | y | z" := (and x .. (and y z) ..) (at level 100).
Notation "'andl:' | x | y | .. | z" := (and .. (and x y) .. z) (at level 100).

Check andl: | True | True.
(* Error: Syntax error: '|' or '|' expected (in [term]).  *)
Check andr: | True | True.
``````

#### Pierre Castéran (Jun 12 2023 at 09:49):

You may give some information about the level of the arguments.

``````Notation "'andr:' | x | .. | y | z " := (and x .. (and y z) ..)
(at level 100, x at next level, y at next level,
z at next level).
Check andr: | True | True.

Goal andr: | True | True | True.
repeat split; trivial. Qed.
``````

#### MackieLoeffel (Jun 12 2023 at 16:45):

Thank you, this solves my problem!

Last updated: Jun 23 2024 at 05:02 UTC