1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
\begin{theindex}
\item \verb+"`+$\dots$\verb+`"+ (string constants), 5--6
\item {\ptt ``\_DEF}, 14
\indexspace
\item {\ptt ASCII\_11}, 2, 3, 6, 14
\item {\ptt ascii\_Axiom}, 1--2, 14
\item {\ptt ascii\_CASES}, 2, 14
\item {\ptt ASCII\_DEF}, 13
\item {\ptt ascii\_EQ\_CONV}, 3, 9
\item {\ptt ascii\_Induct}, 2, 15
\item {\ptt ascii\_ISO\_DEF}, 13
\item {\ptt ascii\_TY\_DEF}, 13
\indexspace
\item case analysis
\subitem on type {\tt ascii}, 2
\subitem on type {\tt string}, 4
\indexspace
\item function definitions
\subitem on type {\tt ascii}, 2
\subitem on type {\tt string}, 4
\indexspace
\item {\ptt load\_string}, 8, 10
\indexspace
\item {\ptt NOT\_EMPTY\_STRING}, 4, 15
\item {\ptt NOT\_STRING\_EMPTY}, 4, 15
\indexspace
\item string constants, 5--6
\item {\ptt STRING\_11}, 4, 6, 15
\item {\ptt string\_Axiom}, 3--4, 15
\item {\ptt string\_CASES}, 4, 15
\item {\ptt string\_CONV}, 5--6, 10
\item {\ptt STRING\_DEF}, 13
\item {\ptt string\_EQ\_CONV}, 6, 11
\item {\ptt string\_Induct}, 4, 15
\item {\ptt string\_ISO\_DEF}, 14
\item {\ptt string\_TY\_DEF}, 14
\item structural induction, 4
\indexspace
\item theorems
\subitem about the type {\tt ascii}, 2
\subitem about the type {\tt string}, 4
\end{theindex}
|
