1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{appendix}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \begin{table}[htbp] |
|
20 \begin{center} |
|
21 \begin{tabular}{lll} |
|
22 Constant & Type & Syntax \\ |
|
23 \hline |
|
24 \isa{{\isadigit{0}}} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}zero} \\ |
|
25 \isa{{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}one} \\ |
|
26 \isa{plus} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}plus\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}plus\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}plus} & (infixl $+$ 65) \\ |
|
27 \isa{minus} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}minus\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}minus\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}minus} & (infixl $-$ 65) \\ |
|
28 \isa{uminus} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}uminus\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}uminus} & $- x$ \\ |
|
29 \isa{times} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}times\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}times\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}times} & (infixl $*$ 70) \\ |
|
30 \isa{divide} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}inverse\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}inverse\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}inverse} & (infixl $/$ 70) \\ |
|
31 \isa{Divides{\isaliteral{2E}{\isachardot}}div} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div} & (infixl $div$ 70) \\ |
|
32 \isa{Divides{\isaliteral{2E}{\isachardot}}mod} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}div} & (infixl $mod$ 70) \\ |
|
33 \isa{abs} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}abs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}abs} & ${\mid} x {\mid}$ \\ |
|
34 \isa{sgn} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}sgn\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}sgn} \\ |
|
35 \isa{less{\isaliteral{5F}{\isacharunderscore}}eq} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ord\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ord\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (infixl $\le$ 50) \\ |
|
36 \isa{less} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ord\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ord\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (infixl $<$ 50) \\ |
|
37 \isa{top} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}top} \\ |
|
38 \isa{bot} & \isa{{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}bot} |
|
39 \end{tabular} |
|
40 \caption{Important Overloaded Constants in Main} |
|
41 \label{tab:overloading} |
|
42 \end{center} |
|
43 \end{table}% |
|
44 \end{isamarkuptext}% |
|
45 \isamarkuptrue% |
|
46 % |
|
47 \isadelimtheory |
|
48 % |
|
49 \endisadelimtheory |
|
50 % |
|
51 \isatagtheory |
|
52 % |
|
53 \endisatagtheory |
|
54 {\isafoldtheory}% |
|
55 % |
|
56 \isadelimtheory |
|
57 % |
|
58 \endisadelimtheory |
|
59 \end{isabellebody}% |
|
60 %%% Local Variables: |
|
61 %%% mode: latex |
|
62 %%% TeX-master: "root" |
|
63 %%% End: |
|