这是 gallina 命令，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
gallina - 从 Coq 白话文件中提取规范
概要
母鸡 [ - [ -标准输出 [ -暂无评论 ] 文件 ...
商品描述
母鸡 将 Coq 文件作为参数并构建相应的规范文件。
Coq 文件 foo.v 承担规范文件 foo.g. 后缀“.g”代表
为了加利纳。
为此，gallina 删除了所有遵循“定理”、“引理”、“事实”、
"Remark" 或 "Goal" 语句，直到它到达命令 "Abort.", "Save.", "Qed.",
“确定。” 或“证明 <...>.”。 它还会删除每个“提示”、“语法”、“立即”或
“透明”命令。
没有 .v 后缀的文件将被忽略。
配置
-标准输出
在标准输出上打印结果。
- Coq 源采用标准输入。 结果打印在标准输出上。
-暂无评论
*.g 文件中的注释被删除。
附注
正确处理嵌套注释。 特别是每个命令“保存”。 或“中止”。 在
不考虑评论。
使用 onworks.net 服务在线使用 gallina
