|
|
|---|
|
|
|
|---|
Source and execution character sets.
These are described in [C:5.2.1].
The members of these sets are more abstract entities than the values of the character types [C:6.2.5/15]. The assignment of values to the members of the execution character set is implementation-defined [C:5.2.1/1], subject to some constraints. The source and execution character sets may be different, subject to certain constraints and correspondences.
Our formalization is parameterized over the specifics of the source and execution character sets. We represent these character sets via suitably constrained ACL2 predicates and mappings.