CODEWITHSUNDEEP
coq
Max Heiber
Max Heiber

Reputation: 15502

Coq: Syntax error 'Type' or 'Types' expected after 'Implicit'

I'm getting Syntax error 'Type' or 'Types' expected after 'Implicit'

when typing in the following from Coq'Art:

Set Implicit Arguments.

CoInductive LList (A: Set) : Set :=
  LNil : LList A
  | LCons : A -> LList A -> LList A.

Implicit Arguments LNil [A].

Here is my Coq version:

$ coqc --version
The Coq Proof Assistant, version 8.12.0 (July 2020)
compiled on Jul 26 2020 6:47:02 with OCaml 4.09.0

What is the right way to accomplish what I want?

I want the type argument to not be required for LNil, and, generally, for the examples in chapter 13 of Coq'Art to work with my version of Coq.

Update

Arguments LNil { A }. seems to work. Now I'm curious about the reason for this change, and if there is any difference in meaning between the new Arguments LNil { A }. and the old Implicit Arguments LNil [A].

Upvotes: 1

Views: 261

Answers (1)

Lucien David
Lucien David

Reputation: 320

I just found this on the reasons of the change : https://coq.inria.fr/refman/changes.html

Removed deprecated commands Arguments Scope and Implicit Arguments in favor of Arguments, with the help of Jasper Hugunin.

The main reason seems to be the generalization of implicit arguments and scope in a same command :

Enrico Tassi introduced a command Arguments that generalizes Implicit Arguments and Arguments Scope for assigning various properties to arguments of constants.

You might find further details at the address, or you could directly contact the commiters.

Upvotes: 2

Related Questions