My proposal of [: :] is suggestive of typing and should be good enough, considering that such “type casts” would seldom be necessary.
Larry > On 6 Jun 2015, at 16:06, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> 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. > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
