The Theory char
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)
fill∧ (∀ r• IsCharRep r ⇔ RepChar (AbsChar r) = r)

up quick index

privacy policy

Created:

V