Stream: Beginner Questions

Topic: jEdit style


view this post on Zulip Robert Soeldner (Apr 22 2021 at 11:48):

Is it possible to mix subscription and superscription? Would like to use \mathcal{M}^{V}_{Rule}. I tried using CTRL+E + arrow as in: ℳ⇧V⇩R⇩u⇩l⇩e
But Isabelle complaints with "Malformed command syntax".

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:55):

If I recall correctly, by convention, subscripts are interpreted as belonging to the same identifier, whereas superscripts are not.

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:55):

The reason being that you often write things like x1x_1 where the index is part of the variable name, but when you have something like x2x^2, the 2{}^2 is an operator acting on the thing before it.

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:56):

Frankly my advice would be to use subscripts and superscripts sparingly.

view this post on Zulip Lukas Stevens (Apr 22 2021 at 11:56):

Can't you nest that stuff with bsub and esub (in theory)? Probably not a good idea though.

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:57):

It will probably still be interpreted as not being part of that identifier.

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:57):

(and bsub/esub is rendered in a not very pretty way by jEdit)

view this post on Zulip Robert Soeldner (Apr 22 2021 at 11:57):

This makes sense, thank you for the fast reply :)

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:57):

You can declare such things as notation. It's done that way e.g. for Z0\mathbb{Z}_{\leq 0}.

view this post on Zulip Manuel Eberl (Apr 22 2021 at 11:58):

That is internally a constant called nonpos_Ints with notation ℤ⇩≤⇩0.


Last updated: Mar 28 2024 at 12:29 UTC