Christian Urban (Jun 13 2022 at 09:22): 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.)
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.
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.
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.
Manuel Eberl (Jun 13 2022 at 11:32):I half-remember some discussion about this on the mailing list from a few years ago.
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.
Thanks a lot! I just assumed it would work for identifiers.
Wolfgang Jeltsch (Jun 13 2022 at 15:20):You should be able to define the variant with block subscripts as special notation, though.
Christian Urban (Jun 14 2022 at 10:41):Thanks Wolfgang! Will try.
Wolfgang Jeltsch (Jun 14 2022 at 15:41):Let me know whether it really works. :smile:
Last updated: Dec 21 2024 at 12:33 UTC