| Parents |
| list |
| Children |
| basic_hol |
| Constants |
|
IsCharRep
|
ℕ → BOOL |
|
AbsChar
|
ℕ → CHAR |
|
RepChar
|
CHAR → ℕ |
| Types |
|
CHAR
|
| Type_Abbreviations |
|
STRING
|
STRING |
| Definitions |
|
IsCharRep
is_char_rep_def
|
⊢ ∀ x• IsCharRep x ⇔ x < 256 |
|
CHAR
char_def
|
⊢ ∃ f• TypeDefn IsCharRep f |
|
AbsChar
RepChar
abs_char_rep_char_def
|
⊢ (∀ a• AbsChar (RepChar a) = a)
 ∧ (∀ r• IsCharRep r ⇔ RepChar (AbsChar r) = r)
|
