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
|
\DOC types
\TYPE {types : (string -> (int # string) list)}
\SYNOPSIS
Lists the types in the named theory.
\DESCRIBE
The function {types} should be applied to a string which is the name of an
ancestor theory (including the current theory; the special string {`-`} is
always interpreted as the current theory). It returns a list of all the
type constructors declared in the named theory, in the form of arity-name
pairs.
\FAILURE
Fails unless the named theory is an ancestor.
\EXAMPLE
The theory {HOL} has no types declared:
{
#types `HOL`;;
[] : (int # string) list
}
\noindent but its ancestors have the following types declared:
{
#itlist union (map types (ancestors `HOL`)) [];;
[(2, `fun`);
(2, `prod`);
(0, `bool`);
(0, `ind`);
(0, `num`);
(1, `list`);
(0, `tree`);
(1, `ltree`);
(2, `sum`);
(0, `one`)]
: (int # string) list
}
\SEEALSO
ancestors, axioms, constants, definitions, infixes, new_type, new_type_abbrev,
new_type_definition, parents.
\ENDDOC
|
