开发者社区

文档建议反馈控制台

文章/答案/技术大牛

发布

社区首页 >问答首页 >utop:错误:引用未定义的全局语法

问utop:错误:引用未定义的全局语法
EN

Stack Overflow用户

提问于 2016-04-19 12:39:19

回答 1查看 454关注 0票数 1

我想检查Coq语法的信息，所以我将grammar.cma加载到utop中：

#load "/home/xxx/.opam/system/lib/coq/grammar/grammar.cma";;

但有个错误：

Error: Reference to undefined global `Grammar'

Coq版本: 8.5.0 OCaml版本: 4.02.3 utop版本: 1.19

EN

回答 1

Stack Overflow用户

回答已采纳

发布于 2016-04-20 00:16:34

我建议您使用Drop命令，这将使您能够访问一个ML进行进一步的开发。

$ coqtop.byte
Coq < Drop.
#

Drop的文档：command137

票数 2

EN

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/36718662

复制

相似问题