Hi All,

I have an existentially quantified variable which I want to give a name like $v_{min}$ in the LaTeX output. I could get this to work

∃! v\<^sub>m\<^sub>i\<^sub>n .......

which is however not quite what I want, but when I tried

∃! v\<^bsub>min\<^esub>....

Isabelle flags this as Inner syntax error. Is there anything wrong with this notation, or does Isabelle not allow this syntax in quantified variables?

Thanks a lot! (Sorry if this has already been answered somewhere else...I could not find it via Google or Manuals.)

I think `\<^bsub> / \<^esub>`

are not allowed in identifiers, similarly to `\<^sup>`

. However, `\<^sub>`

is allowed. This reflects the most common usage.

If you write `x\<^sub>2`

then you probably mean a variable `x`

with a `2`

in the index. If you write `x\<^sup>2`

on the other hand, you probably mean ‘`x`

squared’, i.e. some operator applied to `x`

.

Similarly, `\<^bsub> / \<^esub>`

are used e.g. by HOL-Algebra to specify which group's operation you are talking about.

I half-remember some discussion about this on the mailing list from a few years ago.

Cf. e.g. this NEWS entry:

```
* Pure: There are now sub-/superscripts that can span more than one
character. Text between \<^bsub> and \<^esub> is set in subscript in
ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
superscript. The new control characters are not identifier parts.
```

Thanks a lot! I just assumed it would work for identifiers.

You should be able to define the variant with block subscripts as special notation, though.

Thanks Wolfgang! Will try.

Let me know whether it really works. :smile:

Last updated: Aug 15 2022 at 02:13 UTC