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 2023 at 20:16 UTC