Stream: Beginner Questions

Topic: jEdit style

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".

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.

Manuel Eberl (Apr 22 2021 at 11:55):

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

Manuel Eberl (Apr 22 2021 at 11:56):

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

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.

Manuel Eberl (Apr 22 2021 at 11:57):

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

Manuel Eberl (Apr 22 2021 at 11:57):

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

Robert Soeldner (Apr 22 2021 at 11:57):

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

Manuel Eberl (Apr 22 2021 at 11:57):

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

Manuel Eberl (Apr 22 2021 at 11:58):

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

Last updated: Dec 21 2024 at 16:20 UTC