> On Sat, 12 Mar 2016, Florian Haftmann wrote: > >> * A type of infinitely many characters could serve a model for unicode >> characters. > > Unicode has only finitely many code points. Presently, 21 bits are > sufficient to encode that. > > Does it make sense to have a char type with somewhat "unspecified" size. > I.e. one that might change over the years, like Unicode does?
I had something similar in mind when I wrote this. My idea would be to
have a type of infinitely many characters where only a defined (but
monotonously growing) prefix is associated with glyphs for concrete syntax.
Florian
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://isabelle.in.tum.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
