[isabelle-dev] lifting syntax with proper symbols
kuncar at in.tum.de
Fri Mar 4 14:13:50 CET 2016
As Andreas already mentioned, we've been consistently using the symbol
\Mapsto for ===> in our papers. Concerning --->, we used \mapsto.
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 --->.
> 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
>> locale lifting_syntax
>> notation rel_fun (infixr "===>" 55)
>> notation map_fun (infixr "--->" 55)
>> 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
>> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev