时间戳

首页 > 解决方案 > Coq：在“隐式”之后应出现语法错误“类型”或“类型”

coq - Coq：在“隐式”之后应出现语法错误“类型”或“类型”

问题描述

我越来越Syntax error 'Type' or 'Types' expected after 'Implicit'

从 Coq'Art 输入以下内容时：

Set Implicit Arguments.

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

Implicit Arguments LNil [A].

这是我的 Coq 版本：

$ 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

什么是完成我想要的正确方法？

我希望 LNil 不需要 type 参数，并且一般来说，对于 Coq'Art 第 13 章中的示例，可以与我的 Coq 版本一起使用。

更新

Arguments LNil { A }.似乎工作。现在我很好奇这种变化的原因，以及Arguments LNil { A }.新旧之间的含义是否有任何区别Implicit Arguments LNil [A].

标签： coq

解决方案

我刚刚在更改的原因上发现了这一点： https ://coq.inria.fr/refman/changes.html

在 Jasper Hugunin 的帮助下，删除了已弃用的命令 Arguments Scope 和 Implicit Arguments 以支持 Arguments。

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.

推荐阅读