Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_"

Question

We are very very beginner for coq. The following is code in Basic.v

1 Set Implicit Arguments.
2
3 (* Pretty-print for if-then-else expressions on informative types *)
4
5 Notation "'If' c1 'then' c2 'else' c3" :=
6   match c1 with
7   | left _ => c2
8   | right _ => c3
9   end (at level 200).
10
11  Notation "'IF' c1 'THEN' c2 'ELSE' c3" :=
12  (IF c1 then c2 else c3)(at level 200, v ident).
13
14  Definition IFEXTHENELSE (A : Set) (P1 P2 : A -> Prop) 
15 (P3 : Prop) := (exists2 x : A, P1 x & P2 x) \/ ~ (exists x : A, P1 x) /\ P3.
16
17 Notation "'IFEX' v | c1 'THEN' c2 'ELSE' c3" :=
18 (IFEXTHENELSE (fun v => c1) (fun v => c2) c3) (at level 200, v ident).

We met the following warning during compile of some existing files.

coqc -noglob  -q  -R . K Lib\Basic
Warning: File ".\Lib\Basic" has been implicitly expanded to ".\Lib\Basic.v"
[file-no-extension,filesystem]
File ".\Lib\Basic.v", line 11, characters 0-91:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File ".\Lib\Basic.v", line 11, characters 0-91:
Error: v is unbound in the notation.

There are two warnings and one error.

[file-no-extension,filesystem] .
If you can explain, could you please let us know the meaning of the warning?
Warning: grammar entry "ident" permitted "_" We cannot understand the meaning of the above grammer warning. could you please inform us the meaning?
error. Unbounded.

Thank you very much in advance

Hi! Could you post line 17 in Basic.v (and a few lines above and below it) so we can see the exact error? — Joshua Grosso Reinstate CMs, Jul 21 '21 at 06:54
Thank you for your help. I updated the content to show more exact problem. There are also one error. If you can comment on this, thank you very much. — Wonil Lee, Jul 21 '21 at 07:11

score 0 · Answer 1 · answered Jul 21 '21 at 13:09

You should use Lib\Basic.v instead of Lib\Basic when compiling the file. This will prevent the first warning.
In the first notation, you declared an identifier v even though no such v appears in the notation. Just remove the declaration and the error will go away:
```
 Notation "'IF' c1 'THEN' c2 'ELSE' c3" :=
   (IF c1 then c2 else c3)(at level 200).
```
Finally, in the last notation you declared v as an identifier. Coq is just warning you that the behavior of identifiers is going to change. Right now, you can write something like
```
 IFEX _ | True THEN False ELSE TRUE
```
where the _ indicates that the bound name is not used in the arguments of the if. If you want this behavior, you should instead write
```
 Notation "'IFEX' v | c1 'THEN' c2 'ELSE' c3" :=
  (IFEXTHENELSE (fun v => c1) (fun v => c2) c3) (at level 200, v name).
```
where v ident was replaced by v name. This will still work in future versions of Coq.

Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_"

1 Answers1