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

Notation at level 200 can't be parsed (?) #15695

Open
ana-borges opened this issue Feb 16, 2022 · 1 comment
Open

Notation at level 200 can't be parsed (?) #15695

ana-borges opened this issue Feb 16, 2022 · 1 comment
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.

Comments

@ana-borges
Copy link
Contributor

ana-borges commented Feb 16, 2022

Description of the problem

Inductive t : Set := C : t -> t -> t.
Reserved Notation "a $ b" (at level 200, right associativity).
Infix "$" := C.
Variables (a b : t).
Check (a $ b).
(* Error: Syntax error: ',' or ')' expected after [term level 200] (in [term]). *)

Other levels don't seem to have this problem.

Coq Version

master

cc. @Alizter

@Alizter Alizter added the part: notations The notation system. label Feb 16, 2022
@ana-borges ana-borges added the kind: bug An error, flaw, fault or unintended behaviour. label Feb 16, 2022
@ana-borges
Copy link
Contributor Author

@herbelin: "A notation at level 200 that starts with a variable should be forbidden."

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.
Projects
None yet
Development

No branches or pull requests

2 participants