Search code examples
listcoq

singleton list (`A) in Coq?

I am trying to understand and compile linear logic formalization in Coq: http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ILL.v

Here is this code:

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))
...

But this code does not compile, it is giving error message Syntax Error: Lexer: Undefined token for the code piece `A.

It is said in the accompanying article that ` simbol denotes the singleton list consisting from one element and that the ^ symbol if for the concatenation of the lists.

So - why the recent (CoqIDE 8.6.1) Coq does not recognize those symbols and should I import any addidional theories at the start of ILL.v file?

Solution

  • The syntax that file uses is defined in the moreLists file that is part of the development. However, that paper was written in 1999, and the version of Coq used there has very little to do with the current one. Sadly, it seems that you would need a lot of work to port that development to work now. For instance, back then Coq had a different set of basic tactics, a different standard library, and a different syntax extension mechanism.