search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.84k stars 647 forks source link

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

Open ana-borges opened 2 years ago

ana-borges commented 2 years ago

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

ana-borges commented 2 years ago

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