[isabelle-dev] »real« considered harmful

[Makarius]

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