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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
