Download OCML manual

ii
7
Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
7.1
Functional Term Constructors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.1 setofall . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.2 findall . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.3 the . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.4 in-environment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.5 quote . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.6 if . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1.7 cond . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Control Term Constructors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.1 in-environment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.2 if . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.3 cond . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.4 loop. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.5 do . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.6 repeat. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2.7 return. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.3 Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.4 Inheritance and Default Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8
Interpreters and Proof System . . . . . . . . . . . . . . . 24
8.1
8.2
8.3
8.4
9
20
20
20
20
20
20
20
20
20
20
21
21
21
21
21
21
21
23
Functional term interpreter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Control term interpreter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Proof system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Proof rules for non-basic goal expressions . . . . . . . . . . . . . . . . . . . . . .
24
24
24
25
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
Function Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Concept Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29