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)"
fun test where
"test a x =
(let b = Suc (Suc a); \<comment>\<open>b = a + 2\<close>
c = b + x
in a * b * c)"
it looks less ugly in Isabelle because comment becomes a long hypen
Thanks, exactly what I was looking for!
For future reference, what you call "code" (the stuff that goes between quotation marks) is called the inner syntax.
Last updated: Dec 07 2024 at 16:22 UTC