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

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

Thank you, this solves my problem!

Last updated: Jun 23 2024 at 05:02 UTC