Coq 中的单例列表 (`A)？

Question

我正在尝试理解和编译 Coq 中的线性逻辑形式化：http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ILL.v

这是这段代码：

Inductive LinCons : (list ILinProp) -> ILinProp -> Prop := 
(* Structural Rules *)
 Identity : 
  (A:ILinProp)  
  (`A |- A)
| Exchange : 
  (A,B,C : ILinProp)(D1,D2 : (list ILinProp))
  ((D1 ^ `A ^ `B ^ D2 |- C) -> (D1 ^ `B ^ `A ^ D2 |- C))
...

但是这段代码无法编译，它给出了代码片段 `A.

的错误消息 Syntax Error: Lexer: Undefined token

附文中说`符号表示由一个元素组成的单例列表，^符号表示列表的串联。

那么 - 为什么最近的 (CoqIDE 8.6.1) Coq 不能识别这些符号，我应该在 ILL.v 文件的开头导入任何额外的理论吗？

Answer 1

文件使用的语法在作为开发一部分的 moreLists 文件中定义。然而，那篇论文是在 1999 年写的，那里使用的 Coq 版本与现在的版本关系不大。可悲的是，您似乎需要做很多工作才能将开发移植到现在。例如，当时的 Coq 有一套不同的基本策略、不同的标准库和不同的语法扩展机制。

Coq 中的单例列表 (`A)？

singleton list (`A) in Coq?

list

coq