Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Superscript argument to a function

view this post on Zulip Email Gateway (Jul 28 2020 at 13:46):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Good day,

I have a question concerning the use of superscripts as arguments to
functions. I have a function ccc_rel that has 3 arguments, and I would
like that the syntax for the first one is a superscript. (I'm working in
ZF, don't know if that is relevant.)

If I enter

notation ccc_rel (‹ccc⇧_'(_,_')›)

everything works fine until the first argument has more than one
character. If I use \<bsup>...\<esup> instead:

notation ccc_rel (‹ccc⇗_⇖'(_,_')›)

it accepts a multi-character first argument but it the PIDE does not
prettyprints the superscript.

Can I have the cake and eat it?

PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>

view this post on Zulip Email Gateway (Aug 10 2020 at 07:28):

From: Benedikt Nordhoff <bnord01@gmail.com>
Dear Pedro,

I implemented basic support for this for Isabelle 2014 but it never made it into any release. It worked fine till the 2017 release, I haven’t tried the patch on later versions. If you’re interested and want to try whether the patch still works you can find it here: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html

Best
Benedikt

view this post on Zulip Email Gateway (Aug 13 2020 at 11:33):

From: Benedikt Nordhoff <bnord01@gmail.com>
Dear Pedro,

I’m certainly not the most qualified to answer this. I haven’t build Isabelle from source for quite a while. I think back then I used the README_REPOSITORY file as a guide.

Concerning applying the patch, I’m not familiar with hg but in git I’d try checking out the commit mentioned in the path, apply it there and hope for merge to do it’s magic.

Best Benedikt

view this post on Zulip Email Gateway (Aug 18 2020 at 22:52):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Hello,

Concerning applying the patch, I’m not familiar with hg but in git I’d
try checking out the commit mentioned in the path, apply it there and
hope for merge to do it’s magic.
Just in case I adapted the patch for Isabelle 2020 (last relevant commit
97ccf48c2f0c) and it works for me on some non-trivial theories with
nested subscripts and superscripts (I also don't have any previous
experience with Isabelle/Scala though)

Sample original theory source fragment:
⬚‹
also from Sucinner have
"... = - G κ⇘i+1⇙ κ⇘i+2⇙

+ int (∑x|x<m⇘κ⇘i+1⇙⇙∧x⇧♮∈vars K⇘κ⇘i+1⇙⇙.
MAX⇩0 t∈terms K⇘κ⇘i+1⇙⇙|t~P⇘κ⇘i+2⇙⇙!0. #⇘x⇧♮⇙ t *
size (σ⇘i+1⇙ x⇧♮))

- int (∑x≤(m⇘κ⇘i+1⇙⇙ - 1)⇧♯. #⇩x (P⇘κ⇘i+1⇙⇙!0) * size (σ⇘i+1⇙
x))"
(is "_ + int (∑x∈?S. ?g x) - _ = _ + int (∑x∈?T. ?h x)- _") by
›

Regards,
Mikhail

Benedikt Nordhoff писал 2020-08-13 14:33:

Dear Pedro,

I’m certainly not the most qualified to answer this. I haven’t build
Isabelle from source for quite a while. I think back then I used the
README_REPOSITORY file as a guide.

Best Benedikt

Am 12.08.2020 um 17:36 schrieb Pedro Sánchez Terraf
<sterraf@famaf.unc.edu.ar>:

Dear Benedikt,

Sorry to bother you with an dumb question, but I do not know how to
build jEdit. Could you point me to some docs where I can find this?
(Note: I'm not a computer scientist but I can manage some stuff).
It seems that there have been many some movements and the patch should
be applied somewhere in

Tools/jEdit/src/syntax_style.scala,
but I could be wrong.

Best wishes,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>

El 10/8/20 a las 04:27, Benedikt Nordhoff escribió:

Dear Pedro,

I implemented basic support for this for Isabelle 2014 but it never
made it into any release. It worked fine till the 2017 release, I
haven’t tried the patch on later versions. If you’re interested and
want to try whether the patch still works you can find it here:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html>

Best
Benedikt

Am 28.07.2020 um 15:45 schrieb Pedro Sánchez Terraf
<sterraf@famaf.unc.edu.ar> <mailto:sterraf@famaf.unc.edu.ar>:

Good day,

I have a question concerning the use of superscripts as arguments to
functions. I have a function ccc_rel that has 3 arguments, and I
would like that the syntax for the first one is a superscript. (I'm
working in ZF, don't know if that is relevant.)

If I enter

notation ccc_rel (‹ccc⇧_'(_,_')›)

everything works fine until the first argument has more than one
character. If I use \<bsup>...\<esup> instead:

notation ccc_rel (‹ccc⇗_⇖'(_,_')›)

it accepts a multi-character first argument but it the PIDE does not
prettyprints the superscript.

Can I have the cake and eat it?

PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
sub_sup.patch
sub_sup.png

view this post on Zulip Email Gateway (Aug 19 2020 at 02:48):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
This is great, I hope it makes it into the 2021 release.

PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
El 18/8/20 a las 19:51, Mikhail Mandrykin escribió:

view this post on Zulip Email Gateway (Sep 07 2021 at 14:07):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear Mikhail,

I've been successfully using your patch on Isabelle2020. Though I tried
hard, I couldn't make it work for the current development version (I
only managed to make it work with non-nested scripts). Would you mind
giving me some hints on how to adapt it?

I'm about to present a formalization to other mathematicians and a
smooth notation is key.

Thank you very much in advance,

view this post on Zulip Email Gateway (Sep 08 2021 at 10:23):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Dear Pedro,

I tried updating the patch to the current development version (attached
as ‹sub_sup_devel.patch›). After straightforward rebasing it worked for
me seemingly correctly. I did not fully understand the issue with nested
scripts, though. If you mean long (delimited, multi-symbol)
sub/superscripts, their nesting was actually not supported in the
original patch in a sense that nested script delimiters were hidden, but
ignored, and so the inner font style was unchanged (as to visually merge
with the outer script). Only one-symbol nested scripted were supported.
I tried modifying the patch to support nested delimited scripts
(attached ‹sub_sup_stack.patch›) and it also seems to work (on small
artificial tests), but I have not tested it on any realistic examples
yet

Regards,
Mikhail

Pedro Sánchez Terraf писал 2021-09-07 17:06:
sub_sup_devel.patch
sub_sup_stack.patch

Last updated: Jan 04 2025 at 20:18 UTC