Stream: Coq users

Topic: Problem with right associative recursive notation


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip MackieLoeffel (Jun 12 2023 at 16:45):

Thank you, this solves my problem!


Last updated: Jun 23 2024 at 05:02 UTC