[isabelle-dev] »real« considered harmful

[Larry Paulson]

The first question is, do we need a prefix syntax for type constraints? My point was that the ability to write

	[:real:]of_nat k

might be better than having to introduce and abbreviations such as real_of_nat, but this is not clear. The latter has the advantage that it is automatically introduced when the term has the matching type, and we would not want the pretty printer to insert [:real:] all over the place, but only when it is necessary.

A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on.

Larry

> On 23 Jun 2015, at 21:42, Makarius <makarius at sketis.net> wrote:
> 
> On Sat, 6 Jun 2015, Florian Haftmann wrote:
> 
>>> Conceivably we could introduce a prefix syntax for type constraints, e.g.
>>> 
>>> 	[:real:]of_nat k
>>> 
>>> I’d find such a thing useful from time to time.
>> 
>> My personal favourite would be System-F-style type instantiation
>> 
>> 	of_nat [real] k
>> 
>> instead of type annotations but there are hardly any brackets left which
>> could serve here.
> 
> In theory we have an infinite store of Isabelle symbols, and many usable Unicode points for rendering.  Here is a list of funny brackets to consider: http://stackoverflow.com/questions/13535172/list-of-all-unicodes-open-close-brackets
> 
> For example:
> 
> U+2772 Ps LIGHT LEFT TORTOISE SHELL BRACKET ORNAMENT ❲
> U+2773 Pe LIGHT RIGHT TORTOISE SHELL BRACKET ORNAMENT ❳
> U+3014 Ps LEFT TORTOISE SHELL BRACKET 〔
> U+3015 Pe RIGHT TORTOISE SHELL BRACKET 〕
> 
> 
> In practice this also needs a LaTeX macro, and maybe some ASCII abbreviation for input in the Prover IDE.
> 
> 
> 	Makarius_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev