coq-tex - 云端在线

程序：

您的姓名

coq-tex - 处理嵌入在 LaTeX 文件中的 Coq 短语

概要

Coq-tex [ -o 输出文件 [ -n 行宽 [ -图片 图像 [ -w [ -v [ -sl [
-规则 [ -小 ] 输入文件 ...

商品描述

这款 Coq-tex 过滤器提取嵌入在 LaTeX 文件中的 Coq 短语，评估它们，并
在每个短语之后插入评估结果。

提供了三个 LaTeX 环境以在输入文件中包含 Coq 代码：

coq_示例
\begin{coq_example} 和 \end{coq_example} 之间的短语被评估并
复制到输出文件中。 每个短语后面都跟着对方的回答
顶层循环。

coq_示例*
\begin{coq_example*} 和 \end{coq_example*} 之间的短语被评估并
复制到输出文件中。 顶层循环的响应被丢弃。

coq_eval
\begin{coq_eval} 和 \end{coq_eval} 之间的短语被默默地评估。
它们不会被复制到输出文件中，并且顶层循环的响应
被丢弃。

生成的 LaTeX 代码存储在文件中 文件.v.tex 如果输入文件的名称为
表格 文件.tex，否则输出文件名就是输入文件名
附加了“.v.tex”。

产生的文件 Coq-tex 可以直接用LaTeX处理。 两个 Coq 短语
并且顶层输出以打字机字体排版。

配置

-o 输出文件
指定要存储 LaTeX 输出的文件的名称。 破折号“-”
导致 LaTeX 输出打印在标准输出上。

-n 行宽
设置线宽。 默认值为 72 个字符。 高层的回应
如果循环比线宽长，则折叠。 没有折叠
Coq 输入文本。

-图片 图像
导致文件 图像 被执行以评估 Coq 短语。 默认情况下，
这是命令 科克托普 不指定任何用于评估的路径
Coq 短语。

-w 尽可能使行在空格字符上折叠，避免切词
在输出中。 默认情况下，折叠发生在行宽处，无论单词如何
削减。

-v 详细模式。 在标准输出上打印 Coq 答案。 有用的检测
Coq 短语中的错误。

-sl 倾斜模式。 Coq 的答案是用倾斜的字体写的。

-规则 水平线模式。 Coq 部分写在两条水平线之间。

-小 小字体模式。 Coq 部分以较小的字体编写。

洞穴

\begin... 和 \end... 短语必须单独排成一行，没有字符
在反斜杠之前或右大括号之后。 每个 Coq 短语必须以
'.' 在一行的末尾。 “.”之间接受空格和换行符，但任何
其他字符将导致 coq-tex 忽略短语的结尾，从而导致
不正确地将答案改组到短语中。 （反应“滞后”。）

使用 onworks.net 服务在线使用 coq-tex