Stream: Beginner Questions

Topic: Code comments

Jakob Schulz (Feb 03 2023 at 12:22):

Hi :) is there a way to write comments inside function definitions? For example, something like this:

fun test where
"test a x =
    (let b = Suc (Suc a); (* b = a + 2 *)
    c = b + x
    in a * b * c)"

Mathias Fleury (Feb 03 2023 at 12:26):

fun test where
"test a x =
    (let b = Suc (Suc a); \<comment>\<open>b = a + 2\<close>
    c = b + x
    in a * b * c)"

Mathias Fleury (Feb 03 2023 at 12:27):

it looks less ugly in Isabelle because comment becomes a long hypen

Jakob Schulz (Feb 03 2023 at 13:38):

Thanks, exactly what I was looking for!

Manuel Eberl (Feb 08 2023 at 21:16):

For future reference, what you call "code" (the stuff that goes between quotation marks) is called the inner syntax.

Last updated: Apr 25 2024 at 12:23 UTC