equal
deleted
inserted
replaced
3 |
3 |
4 theory logic imports base begin |
4 theory logic imports base begin |
5 |
5 |
6 chapter {* Primitive logic *} |
6 chapter {* Primitive logic *} |
7 |
7 |
8 section {* Syntax *} |
8 section {* Variable names *} |
9 |
9 |
10 subsection {* Variable names *} |
10 text FIXME |
|
11 |
|
12 |
|
13 section {* Types \label{sec:types} *} |
11 |
14 |
12 text {* |
15 text {* |
13 FIXME |
16 \glossary{Type class}{FIXME} |
|
17 |
|
18 \glossary{Type arity}{FIXME} |
|
19 |
|
20 \glossary{Sort}{FIXME} |
|
21 |
|
22 FIXME classes and sorts |
|
23 |
|
24 |
|
25 \glossary{Type}{FIXME} |
|
26 |
|
27 \glossary{Type constructor}{FIXME} |
|
28 |
|
29 \glossary{Type variable}{FIXME} |
|
30 |
|
31 FIXME simple types |
14 *} |
32 *} |
15 |
33 |
16 |
34 |
17 subsection {* Simply-typed lambda calculus *} |
35 section {* Terms \label{sec:terms} *} |
18 |
36 |
19 text {* |
37 text {* |
|
38 \glossary{Term}{FIXME} |
20 |
39 |
21 FIXME |
40 FIXME de-Bruijn representation of lambda terms |
22 |
|
23 \glossary{Type}{FIXME} |
|
24 \glossary{Term}{FIXME} |
|
25 |
|
26 *} |
41 *} |
27 |
42 |
28 subsection {* The order-sorted algebra of types *} |
|
29 |
|
30 text {* |
|
31 |
|
32 FIXME |
|
33 |
|
34 \glossary{Type constructor}{FIXME} |
|
35 |
|
36 \glossary{Type class}{FIXME} |
|
37 |
|
38 \glossary{Type arity}{FIXME} |
|
39 |
|
40 \glossary{Sort}{FIXME} |
|
41 |
|
42 *} |
|
43 |
|
44 |
|
45 subsection {* Type-inference and schematic polymorphism *} |
|
46 |
43 |
47 text {* |
44 text {* |
48 |
45 |
49 FIXME |
46 FIXME |
50 |
47 |
53 \glossary{Type variable}{FIXME} |
50 \glossary{Type variable}{FIXME} |
54 |
51 |
55 *} |
52 *} |
56 |
53 |
57 |
54 |
58 section {* Theory *} |
55 section {* Theorems \label{sec:thms} *} |
59 |
|
60 text {* |
|
61 |
|
62 FIXME |
|
63 |
|
64 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the |
|
65 theory context, but slightly more flexible since it may be used at |
|
66 different type-instances, due to \seeglossary{schematic |
|
67 polymorphism.}} |
|
68 |
|
69 *} |
|
70 |
|
71 |
|
72 section {* Deduction *} |
|
73 |
56 |
74 text {* |
57 text {* |
75 |
58 |
76 FIXME |
59 FIXME |
77 |
60 |
137 subsection {* Equational reasoning *} |
120 subsection {* Equational reasoning *} |
138 |
121 |
139 text FIXME |
122 text FIXME |
140 |
123 |
141 |
124 |
142 section {* Proof terms *} |
125 section {* Low-level specifications *} |
143 |
126 |
144 text FIXME |
127 text {* |
|
128 |
|
129 FIXME |
|
130 |
|
131 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the |
|
132 theory context, but slightly more flexible since it may be used at |
|
133 different type-instances, due to \seeglossary{schematic |
|
134 polymorphism.}} |
|
135 |
|
136 \glossary{Axiom}{FIXME} |
|
137 |
|
138 \glossary{Primitive definition}{FIXME} |
|
139 |
|
140 *} |
145 |
141 |
146 end |
142 end |