1

我们是 coq 的初学者。以下是 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).

我们在编译一些现有文件时遇到了以下警告。

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.

有两个警告和一个错误。

  1. [文件无扩展名，文件系统]。
    如果你能解释一下，你能告诉我们警告的含义吗？

  2. 警告：语法条目“ident”允许“_”我们无法理解上述语法警告的含义。你能告诉我们意思吗？

  3. 错误。无界。

非常感谢您提前

4

1 回答 1

0

  1. 您应该在编译文件时使用Lib\Basic.v而不是。Lib\Basic这将阻止第一次警告。

  2. 在第一个符号中，您声明了一个标识符，v即使v符号中没有出现这样的标识符。只需删除声明，错误就会消失：

     Notation "'IF' c1 'THEN' c2 'ELSE' c3" :=
   (IF c1 then c2 else c3)(at level 200).

  3. 最后，在您声明v为标识符的最后一个符号中。Coq 只是警告你标识符的行为将会改变。现在，你可以写类似

     IFEX _ | True THEN False ELSE TRUE

    其中_表示绑定名称未在 的参数中使用if。如果你想要这种行为，你应该写

     Notation "'IFEX' v | c1 'THEN' c2 'ELSE' c3" :=
  (IFEXTHENELSE (fun v => c1) (fun v => c2) c3) (at level 200, v name).

    在哪里v ident被v name. 这在 Coq 的未来版本中仍然有效。

于 2021-07-21T13:09:33.697 回答