CODEWITHSUNDEEP
isabelle
TomR
TomR

Reputation: 3056

How to make multiline comments for Isabelle theory?

Rosetta provides documentation only for the single-line comments for Isabelle https://rosettacode.org/wiki/Comments#Isabelle

I read https://euromils-project.technikon.com/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper-October2015.pdf Section 2.2.4 that suggests text{* ... } or --{ ... *} for the multiline comments but they are not working in my theory:

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

gives

Malformed command syntax

for both blocks of eventually commented code.

Upvotes: 0

Views: 940

Answers (1)

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5780

There are 2 kinds of comments in Isabelle:

  1. Source comments. They are removed from the source code:

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

  2. Document comments. They become part of the document when the Isabelle document preparation mechanism is used. In the simplest form they look like:

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

    Note that the leading symbol is a long dash (it can be inserted as \<comment>) and the angle brackets are also special, not just < and > (they can be inserted as \<open> and \<close>).

The variant with text {* ... *} is not a comment, but a part of the document text, used when generating the document from the theory:

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

Isabelle 2021 warns about the syntax and suggests using cartouche (the brackets ‹...› mentioned above):

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

Note. The original example misses a closing double quote after the final return ()).

Upvotes: 2

Related Questions