[isabelle-dev] Abbreviation for \<leftarrow>
makarius at sketis.net
Wed Mar 5 16:25:18 CET 2014
On Wed, 5 Mar 2014, Lars Noschinski wrote:
> it would be nice if we could also get "<-" as abbreviation for
> \<leftarrow> (and probably <-- for \<longleftarrow) by default.
> \<leftarrow> is regularly used in Monad syntax and list comprehensions
> and it would be nice to have the abbreviations matching the
I can't say on the spot how it would work out: the current scheme is the
result of intensive experimentation over some weeks last summer. This
needs to be repeated soon, when the semantic completion is fully
operational. Right now I am reworking again some details of that.
Did you try any of the catch-all abbreviations, like <. for left arrows,
or .> for right arrows, or <> for double arrows? These are very
ambiguous, but the persistent completion history will move your favourite
arrows to front, for quick access in the popup. Ambiguous completions are
never immediate, though.
It is also possible to add more abbreviations in
$ISABELLE_HOME_USER/etc/settings, although I consider that as something
for expert users only.
More information about the isabelle-dev