UP

The Theory char

Parents

list

Children

basic_hol

Constants

IsCharRepnat func1 BOOL
RepCharCHAR func1 nat
AbsCharnat func1 CHAR

Types

CHAR

Type Abbreviations

STRINGCHAR LIST

Definitions

IsCharRep
is_char_rep_def turnstil forall xspot IsCharRep x equiv x < 256
CHAR
char_defturnstil exists fspot TypeDefn IsCharRep f
AbsChar
RepChar
abs_char_rep_char_def turnstil (forall aspot AbsChar (RepChar a) = a)
and (forall rspot IsCharRep r equiv RepChar (AbsChar r) = r)

HOME net links © RBJ created 1999/11/02 modified 1999/11/02