56 * Characters (type char) are modelled as finite algebraic type |
56 * Characters (type char) are modelled as finite algebraic type |
57 corresponding to {0..255}. |
57 corresponding to {0..255}. |
58 |
58 |
59 - Logical representation: |
59 - Logical representation: |
60 * 0 is instantiated to the ASCII zero character. |
60 * 0 is instantiated to the ASCII zero character. |
61 * All other characters are represented as »Char n« |
61 * All other characters are represented as "Char n" |
62 with n being a raw numeral expression less than 256. |
62 with n being a raw numeral expression less than 256. |
63 * Expressions of the form »Char n« with n greater than 255 |
63 * Expressions of the form "Char n" with n greater than 255 |
64 are non-canonical. |
64 are non-canonical. |
65 - Printing and parsing: |
65 - Printing and parsing: |
66 * Printable characters are printed and parsed as »CHR ''…''« |
66 * Printable characters are printed and parsed as "CHR ''\<dots>''" |
67 (as before). |
67 (as before). |
68 * The ASCII zero character is printed and parsed as »0«. |
68 * The ASCII zero character is printed and parsed as "0". |
69 * All other canonical characters are printed as »CHAR 0xXX« |
69 * All other canonical characters are printed as "CHAR 0xXX" |
70 with XX being the hexadecimal character code. »CHAR n« |
70 with XX being the hexadecimal character code. "CHAR n" |
71 is parsable for every numeral expression n. |
71 is parsable for every numeral expression n. |
72 * Non-canonical characters have no special syntax and are |
72 * Non-canonical characters have no special syntax and are |
73 printed as their logical representation. |
73 printed as their logical representation. |
74 - Explicit conversions from and to the natural numbers are |
74 - Explicit conversions from and to the natural numbers are |
75 provided as char_of_nat, nat_of_char (as before). |
75 provided as char_of_nat, nat_of_char (as before). |