Stream: General

Topic: Problems with \<^bsub>...\<^esub>


view this post on Zulip Christian Urban (Jun 13 2022 at 09:22):

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

view this post on Zulip Manuel Eberl (Jun 13 2022 at 11:30):

I think \<^bsub> / \<^esub> are not allowed in identifiers, similarly to \<^sup>. However, \<^sub> is allowed. This reflects the most common usage.

view this post on Zulip Manuel Eberl (Jun 13 2022 at 11:31):

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.

view this post on Zulip Manuel Eberl (Jun 13 2022 at 11:31):

Similarly, \<^bsub> / \<^esub> are used e.g. by HOL-Algebra to specify which group's operation you are talking about.

view this post on Zulip Manuel Eberl (Jun 13 2022 at 11:32):

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

view this post on Zulip Manuel Eberl (Jun 13 2022 at 11:34):

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.

view this post on Zulip Christian Urban (Jun 13 2022 at 12:56):

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

view this post on Zulip Wolfgang Jeltsch (Jun 13 2022 at 15:20):

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

view this post on Zulip Christian Urban (Jun 14 2022 at 10:41):

Thanks Wolfgang! Will try.

view this post on Zulip Wolfgang Jeltsch (Jun 14 2022 at 15:41):

Let me know whether it really works. :smile:


Last updated: Aug 15 2022 at 02:13 UTC