Stream: Beginner Questions

Topic: Explicit syntax: multi-character \<sub> and \<sup> ?


view this post on Zulip Max Nowak (May 09 2021 at 19:57):

I'm looking to pimp my syntax, turn things such as seq m T n into m \triangleright^{T} n, but by the looks of it whenever T is more than one character, only the first character gets printed in the super position. Is this just a limitation of Isabelle, or can I fix it somehow?

view this post on Zulip Max Nowak (May 09 2021 at 20:00):

seq m TTTT n sadly is rendered as: grafik.png

view this post on Zulip Max Nowak (May 09 2021 at 20:29):

Additional side issue: Defining a syntax such as _\<sub>e will render correctly, but will fail to parse when found in code. It looks like Isabelle is trying to parse all of m\<sub>e as one identifier, since doing (m)\<sub>e does seem to work. Context: Nothing hugely important, just trying to make accessors into a triple prettier (e being one of the triple elements).

view this post on Zulip Max Nowak (May 09 2021 at 20:30):

I guess for now I can just do _!e instead, but that is not as neat :D

view this post on Zulip Mathias Fleury (May 10 2021 at 03:35):

\<^bsup>...\<^esup> but I never remember if Isabelle/jEdit can print that....

view this post on Zulip Mathias Fleury (May 10 2021 at 03:42):

After checking: Isabelle/jEdit is not able print \<^bsup>...\<^esup> correctly, but \<^bsup>...\<^esup> is how you are supposed to do it for LaTeX output

view this post on Zulip Mathias Fleury (May 10 2021 at 03:42):

image.png

view this post on Zulip Max Nowak (May 10 2021 at 09:47):

That is at least a step up from what I had before, so good enough for me, thanks! :)


Last updated: Sep 25 2021 at 08:21 UTC