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