Email Gateway (Aug 23 2022 at 08:20): Email Gateway (Aug 23 2022 at 08:20):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Isabelle/HOL has a special LaTeX syntax for repeated function
composition: while you write f ^^ n in your source text, generated
formulas will have f with a superscript n in LaTeX-generated
output.
Unfortunately, this feature apparently only affects the output of
antiquotations, not the contents of specification. For example, if I
have f ^^ n in an inductive specification, it will show up in LaTeX-
generated output as exactly that.
Is there a way to have the superscript notation within specifications as
well? I tried to write f⇗n⇖ in the source text, but this is not
permitted.
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:21):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
I don't know if this precisely fits your needs, but \<^sub> and \<^sup> are permissible in many places where ⇗ and ⇖ are not. Perhaps f\<^sup>n will work for you?
Email Gateway (Aug 23 2022 at 08:21):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Well, this doesn’t work, because the Isabelle/HOL library doesn’t define
such a notation for function exponentiation. Of course, I could define
it myself, as I could define a notation using ⇗ and ⇖. However, I was
wondering whether I could convince Isabelle to use the ⇗–⇖-notation that
is already established for generated (pretty-printed) output.
All the best,
Wolfgang
Last updated: Apr 26 2024 at 08:19 UTC