Re: [isabelle-dev] lifting syntax with proper symbols
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 (\\<^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-...@in.tum.de > >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > >> > >> > > ___ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lifting syntax with proper symbols
As Andreas already mentioned, we've been consistently using the symbol \Mapsto for ===> in our papers. Concerning --->, we used \mapsto. 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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lifting syntax with proper symbols
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] lifting syntax with proper symbols
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
