我最近在阅读 Álvaro Pelayo、Michael A. Warren 的文章同伦类型理论和 Voevodsky 的单价基础。有一个配套文件http://mawarren.net/papers/tutorial.v。我用最新的 coq 版本 8.8.0 编译它，但遇到了错误。谁能帮我？提前致谢。
问问题
65 次
1 回答
1
此代码旨在使用禁用 Universe 检查的 Coq 8.4 或 Coq 8.3 的自定义补丁版本构建；我记得当时与 Dan Grayson 或 Vladimir 交谈过，他们提到使用这样一个补丁版本的 Coq。（另请注意，该文件来自 2012 年 8 月，并且https://coq.inria.fr/news/说 Coq 8.4 在那个月发布。）很不幸，您引用的文章似乎没有提到版本Coq 的任何地方。
在任何情况下，您都可以在 Coq 8.5 和更高版本中构建此文件，方法是将参数传递-type-in-type给coqcorcoqtop并添加
Set Asymmetric Patterns.
在文件的顶部。如果您使用 ProofGeneral，则可以添加
(* -*- coq-prog-args: ("-type-in-type") -*- *)
到文件的顶部，这样您就不必手动传递-type-in-type到coqtop.
于 2018-05-10T00:42:23.753 回答