coqtop - 云端在线

程序：

您的姓名

coqtop - Coq 证明助手顶层系统

概要

科克托普 [ 选项 ]

商品描述

科克托普 是 Coq 的顶层系统，用于交互使用。 它读取短语
标准输入，并在标准输出上打印结果。

对于 Coq 的面向批处理的使用，请参见 考克（1）。

配置

-H， - 帮帮我
帮助。 将为您提供 coqtop 接受的完整选项列表。

-I 是， - 包括 DIR
添加目录 DIR 在包含路径中

-R DIR 目录
递归映射物理 DIR 合乎逻辑 目录

-最佳 目录
将顶级名称设置为 目录 而不是顶部

-输入状态 文档名称， -是 文件名
从文件中读取状态 文件名.coq

-噪音 从一个空的初始状态开始

-输出状态文件名
在文件中写入状态 文件名.coq

-load-ml-对象 文件名
加载机器学习目标文件 文件名

-load-ml-源 文件名
加载 ML 文件 文件名

-load-vernac-源 文档名称， -l 文件名
加载 Coq 文件 文件名.v （加载文件名。）

-加载vernac源详细 文档名称， -lv 文件名
详细加载 Coq 文件 文件名.v （加载详细文件名。）

-加载-vernac-对象 文件名
加载 Coq 对象文件 文件名.vo

-要求 文件名
加载 Coq 对象文件 文件名.vo 并导入它（需要导入文件名。）

-编译 文件名
编译 Coq 文件 文件名.v （暗示 -批 )

-编译详细 文件名
详细编译 Coq 文件 文件名.v （暗示 -批 )

-选择 运行 Coq 的原生代码版本

-字节 运行 Coq 的字节码版本

-在哪里 打印 Coq 的标准库位置并退出

-v 打印 Coq 版本并退出

-q 跳过 rcfile 的加载

-init-文件 文件名
将 rcfile 设置为 文件名

-批 批处理模式（在参数解析后立即退出）

-启动 启动模式（意味着 -q 和 -批 )

-emacs 告诉 Coq 它是在 Emacs 下执行的

-转储球 文件名
在文件 f 中转储全球化（供 文件(1) )

-带地理证明 （是|否）
在 Coqide 中（取消）激活 Geoproof 的特殊功能（默认为 含 )

- 谓语集
设置排序 设置非谓语

- 不加载证明
不要在内存中加载不透明的证明

-xml 将 XML 文件导出到以目录为根的层次结构
$COQ_XML_LIBRARY_ROOT（如果设置）或标准输出（如果未设置）

品质
提高某些策略产生的证明条款的易读性

使用 onworks.net 服务在线使用 coqtop