[isabelle-dev] lifting syntax with proper symbols

[Andreas Lochbihler]

Hi Makarius,

How about LaTeX \Mapsto for ===>? This is what I use in my papers following Ondrej and 
Brian's paper on lifting.

I'd be happy to have syntax for ===> enabled by default, as it makes transfer and 
parametricity rules much easier to read. I have no opinion on --->.

Andreas

On 04/03/16 11:56, Makarius wrote:
> Isabelle2016 has removed quite a lot of old ASCII syntax, and made Isabelle symbols the
> default where old ASCII syntax is still available.
>
> A notable exception is lifting_syntax with its old-style ASCII-only notation, see
> http://isabelle.in.tum.de/repos/isabelle/annotate/aeee0a4be6cf/src/HOL/Transfer.thy#l19
>
> locale lifting_syntax
> begin
>    notation rel_fun (infixr "===>" 55)
>    notation map_fun (infixr "--->" 55)
> end
>
>
> I can imagine two reforms:
>
>    * Use proper symbols for these operators (without keeping ASCII
>      replacement syntax).
>
>    * Make the notation a global default, i.e. remove the locale and its
>      interpretations in applications.
>
>
> The usual question is which symbols are best.
>
> ===> appears to be more frequently used than --->. Based on that observation, the new
> triple-line arrow ⇛ could be used for ===>, and maybe a bold → for --->.
>
> This is only a first idea. There are many possibilities. It is also possible to add new
> glyphs to the Isabelle fonts, as long as there are canonical LaTeX macros for that and
> some code points in the Unicode charts that many be (ab)used for our application.
>
> Recent examples of Unicode ab-use in Isabelle symbol interpretation are:
>
> ⤏
> ⇢
> ⤜
> ⪢
>
> These need to be viewed in Isabelle/jEdit to see the point: the official shape of the
> glyph serves as crude approximation for the intended meaning in Isabelle.
>
>
>      Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>