Email Gateway (Aug 18 2022 at 18:17): Email Gateway (Aug 18 2022 at 18:17):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
I was trying to introduce some additional notation for linear
functionals in vector spaces; the idea is to use:
"[x, f]" as an alternative notation for "f x", where "f" is a linear
functional (let's say, type "'a => 'b") and "x" is an element of type
"'a" (note that the arguments f and x are interchanged in the proposed
notation).
I would like that all notation available for "f x" would still work
for the new notation "[x, f]", in such a way that
[x, f] \oplus [y, f]
would be equivalent to (without unfolding any particular definition):
f x \oplus f y
Is it possible to reach these behavior? How? Maybe brackets are
already a bit overloaded in terms of notation (lists, propositions...)
so a notation based for instance in "<x, f >" would be also
acceptable.
I tried the following approach (which does not interchange arguments)
abbreviation
app :: "('b => 'a) => 'b => 'a" ("<(_),(_)>" 90)
where "<f, x> == f x"
but then when I write, for instance, "term <f, x>" the system does not
seem to find the correct type of the expression.
Thanks for any hint,
Jesus
Email Gateway (Aug 18 2022 at 18:18):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Jesus,
do you need your notation only as input syntax or do you want Isabelle to print
function application this way, too? If it is for input only, you just have to
restrict your abbreviation to the input parser and it works fine:
abbreviation (input)
app :: "('b => 'a) => 'b => 'a" ("<(_),(_)>" 90)
where "<f, x> == f x"
term "<f, x>"
Without the (input) restriction, Isabelle's pretty printer loops when it tries
to display the term again. I do not recommend that you use such syntax
translations for output, because such a translation would apply to all function
applications, which is probably not what you want. You could, however, restrict
your translation to certain type classes (e.g., arbitrary functions from vector
spaces to vector spaces). Still, you will have to install your own print
translation to guarantee termination of the pretty printer.
By the way, any notation that works for "f x" also works for "[x, f]" even "[x,
f]" is a proper constant instead of an abbreviation.
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC