Email Gateway (Aug 23 2022 at 09:26): Email Gateway (Aug 23 2022 at 09:26):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>
Last updated: Apr 20 2024 at 08:16 UTC