这是命令 coqide.byte 可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
coqide - Coq 证明助手图形界面
概要
科奇德 [ 选项 ]
商品描述
科奇德 是 Coq 证明助手的 gtk 图形界面。
对于 Coq 的面向命令行的使用，请参见 科克托普(1) ; 有关 Coq 的批量使用，请参阅
考克（1）。
配置
-h 显示接受的选项的完整列表 科奇德.
-I DIR, -包括 DIR
在包含路径中添加目录 dir。
-R DIR 目录
递归映射物理 DIR 合乎逻辑 目录.
-src 在包含路径中添加源目录。
-是 f, -输入状态 f
从中读取状态 f.coq。
-噪音 从空状态开始。
-输出状态 f
在文件中写入状态 f.coq。
-load-ml-对象 f
加载机器学习目标文件 f.
-load-ml-源 f
加载机器学习文件 f.
-l f, -load-vernac-源 f
加载 Coq 文件 f.v（加载 f。）
-lv f, -加载vernac源详细 f
加载 Coq 文件 f.v（加载详细 f。）
-加载-vernac-对象 f
加载 Coq 对象文件 f.vo。
-要求 f
加载 Coq 对象文件 f.vo 并导入它（需要 f。）
-编译 f
编译 Coq 文件 f.v（意味着 -批).
-编译详细 f
详细编译 Coq 文件 f.v（意味着 -批).
-选择 运行 Coq 或 Coq_SearchIsos 的原生代码版本。
-字节 运行 Coq 或 Coq_SearchIsos 的字节码版本。
-在哪里 打印 Coq 的标准库位置并退出。
-v 打印 Coq 版本并退出。
-q 跳过 rcfile 的加载。
-init-文件 f
将 rcfile 设置为 f.
-批 批处理模式（在参数解析后退出）。
-启动 启动模式（暗示 -q 和 -批).
-emacs 告诉 Coq 它是在 Emacs 下执行的。
-转储球 f
在文件中转储全球化 f （供 文件（1））。
- 谓语集
设置排序 设置非谓语。
- 不加载证明
不要在内存中加载不透明的证明。
-xml 将 XML 文件导出到以目录为根的层次结构
COQ_XML_LIBRARY_ROOT （如果设置）或标准输出（如果未设置）。
使用 onworks.net 服务在线使用 coqide.byte
