Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"only printing" and levels #12589

Open
maximedenes opened this issue Jun 25, 2020 · 1 comment
Open

"only printing" and levels #12589

maximedenes opened this issue Jun 25, 2020 · 1 comment
Labels
part: notations The notation system.

Comments

@maximedenes
Copy link
Member

I was surprised to see that this is accepted:

Notation "!!" := False (at level 0, only printing).
Notation "!!" := False (at level 1).

while the following is rejected:

Notation "!!" := False (at level 0, only printing).
Notation "!!" := False (at level 1, only printing).

Is it expected?

Cc @herbelin

@maximedenes maximedenes added the part: notations The notation system. label Jun 25, 2020
@herbelin
Copy link
Member

herbelin commented Jun 25, 2020

This evolved, but apparently not consistently. There have been requests for supporting an arbitrary number of only printing notations at arbitrary levels (thus consciously losing any kind of reversibility of the parsing).

Consistently with these requests, the second one, as well as:

Notation "!!" := False (at level 1).
Notation "!!" := False (at level 0, only printing).

should a priori be accepted (or, at least, they should be accepted if the rhs is a distinct pattern).

Added: and if the rhs is the same pattern, issuing an overriding warning.

herbelin referenced this issue Jun 25, 2020
We do two changes:
- We distinguish between a notion of format generically attached to
  notations and a new notion of format attached to interpreted
  notations. "Reserved Notation" attaches a format
  generically. "Notation" attaches the format specifically to the given
  interpretation, and additionally, attaches it generically if it is the
  first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
  a specific format.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
part: notations The notation system.
Projects
None yet
Development

No branches or pull requests

2 participants