[isabelle-dev] »real« considered harmful
makarius at sketis.net
Tue Jun 23 22:42:47 CEST 2015
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
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.
More information about the isabelle-dev