如何对伊莎贝尔理论进行多行评论？

Question

Rosetta 仅为 Isabelle 的单行注释提供文档 https://rosettacode.org/wiki/Comments#Isabelle

我阅读了 https://euromils-project.technikon.com/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper-October2015.pdf 第 2.2.4 节建议文本{* ... } 或 --{ ... *} 用于多行注释，但它们在我的理论中不起作用：

theory Max_Of_Two_Integers
  imports Main
begin

function two_integer_max :: "nat ⇒ nat ⇒ nat"
  where
 "two_integer_max first second =
     (if (first > second)  then
        return ()
      else
        return ())
--{* "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second)"
*}
text{* "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second)"
*}

end

给予

Malformed command syntax

对于最终注释代码的两个块。

Answer 1

伊莎贝尔有两种评论：

来源评论。它们已从源代码中删除：

(* "two_integer_max first second =
      (if (first > second) then
        return first
      else
        return second)"
*)

文档注释。当使用 Isabelle 文档准备机制时，它们成为文档的一部分。在最简单的形式中，它们看起来像：
```
― ‹ "two_integer_max first second =
     (if (first > second) then
        return first
      else
        return second)"
›
```
注意前导符号是一个长破折号（可以插入为\<comment>），尖括号也很特殊，不仅仅是<和>（它们可以插入为 \<open> 和 \<close>).

带有text {* ... *}的变体不是注释，而是文档文本的一部分，在理论生成文档时使用：

text {* "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second)"
*}

Isabelle 2021 警告语法并建议使用 cartouche（上面提到的括号 ‹...›）：

text ‹ "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second)"
›

注意。 原始示例在最后的 return ()).

后遗漏了一个结束双引号

如何对伊莎贝尔理论进行多行评论？

How to make multiline comments for Isabelle theory?

isabelle