Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Peter Lammich <Views@gmx.de>
Hi,
I have some
locale X =
fixes e :: "'a => 'a" ("e\<^sub>_")
so that for instance e\<^sub>x gets mapped to this symbol.
Now I want also inputs like "e\<^bsub> f a b <^esub>" to be mapped to this
symbol. How to do that on syntactical level, without fixing and defining a
second symbol in the locale ?
thanks for any help in advance.
--peter
Email Gateway (Aug 17 2022 at 14:15):From: Makarius <makarius@sketis.net>
On Fri, 24 Mar 2006, Peter Lammich wrote:
locale X =
fixes e :: "'a => 'a" ("e\<^sub>_")
Note that \<^sub> cannot really be used like this, because it operates on
a single symbol only. The argument filled in for 'a can be anything, not
just variables of > 1 letters, but arbitrarily complex terms.
Now I want also inputs like "e\<^bsub> f a b <^esub>" to be mapped to
this symbol.
Better use this form exclusively. Proof General provides a key sequence
that makes it as easy to enter as \<^sub> (see describe-mode).
Makarius
Last updated: May 03 2024 at 08:18 UTC