Stream: Beginner Questions

Topic: @{const} antiquotation before definition


view this post on Zulip Jakub Kądziołka (Mar 18 2021 at 23:59):

I would like to introduce the constant that's about to be defined in my text. I'd rather make sure that the name in the text matches the actual name, so I want to use the @{const} antiquotation. However, this doesn't work, because the definition is below the text. Is there any workaround?

I'd also like to be able to give an example with @{lemma}, but it suffers from the same problem.

Of course, I could move the description below the definition, but I would really rather avoid that, as that's opposite of the natural reading order.

view this post on Zulip Lukas Stevens (Mar 19 2021 at 12:26):

I think that is just not possible with Isabelle's document model. It is monotone. You can write the name of the definition in cartouches to approximate the behaviour.


Last updated: Aug 13 2022 at 05:18 UTC