如何在伊莎贝尔中写下标？

问题描述

如何在 Isabelle (2021) text 命令中编写下标？

我尝试使用 <^sub> 符号（它会自动转换为向下箭头），如下所示：

text ‹
identity 1<^sub>S
›

但它给出了一个错误：

Undefined document antiquotation: "sub"⌂

我也尝试过 LaTex 方式并使用下划线 _，但 jEdit 似乎无法识别 LaTex。

解决方法

您可以使用反引号 text：

text ‹
identity \<^text>‹1⇩S›
›
(*or simply*)
text‹identity ‹1⇩S››

有关命令 text 的更多信息，请参阅 Isabelle2021 的官方文档（The Isabelle/Isar Reference Manual 或 Isar-ref）中的第 4.1 小节，了解有关反引用的更多信息{ {1}} 参见 Isabelle2021 的官方文档 (Isar-ref) 中的第 4.2 节。

我也尝试过 LaTex 方式并使用下划线 _，但 jEdit 没有 似乎认得 LaTex。

此外，请注意，通常在处理会话时会生成 LaTeX 输出，并且可以使用任意 LaTeX 源代码来扩充理论文件，如下所示：

text

在这种情况下，text‹identity $1_S$› 应该按预期出现在生成的 LaTeX 文档中。但是，当然，jEdit 会将其显示为原始 LaTeX。如需更多信息，请参阅文档 The Isabelle/Isar Implementation（Isabelle2021 官方文档的一部分），可能还有 LaTeX Sugar for Isabelle 文档（也是 Isabelle2021 官方文档的一部分） ).