|
|
|---|
|
|
|
|---|
Fixtype of Unicode characters.
This is a product type introduced by fty::defprod.
The following invariant is enforced on the fields:
(<= codepoint 1114111)
This is the set of Unicode code points.
We wrap the code point into a one-component product type for better encapsulation and abstraction. We use an invariant to restrict the number to the prescribed range.
This fixtype has currently the same definition as char in the abstract syntax formalization. However, in the future we might change the representation of char (e.g. by keeping track of escapes, or by treating ASCII and non-ASCII differently for more readability), while the fixtype defined here is expected to stay isomorphic to the natural numbers that represent Unicode code points.