[isabelle-dev] lifting syntax with proper symbols

[Peter Lammich]

On Fr, 2016-03-04 at 14:13 +0100, Ondřej Kunčar wrote:
> As Andreas already mentioned, we've been consistently using the symbol 
> \Mapsto for ===> in our papers. Concerning --->, we used \mapsto.

In context of the Refinement Framework, I also use infix syntax for
rel_prod (\<times>\<^sub>r), which, depending on how much uncurried
functions or functions that return tuples you use, makes the difference
between nicely readable and completely unreadable relations.

--
  Peter



> 
> Ondrej
> 
> On 03/04/2016 12:36 PM, Andreas Lochbihler wrote:
> > 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
> >>
> >>
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev