> 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.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
