types
Theory.types : string -> (string * int) list
Lists the types in the named theory.
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, or the current theory.
Example
> load "bossLib";
val it = (): unit
> itlist union (map types (ancestry "-")) [];
val it =
[("hrat", 0), ("hreal", 0), ("real", 0), ("bit0", 1), ("bit1", 1),
("cart", 2), ("finite_image", 1), ("ordering", 0), ("char", 0),
("recspace", 1), ("cv", 0), ("one", 0), ("sum", 2), ("option", 1),
("list", 1), ("prod", 2), ("bool", 0), ("fun", 2), ("ind", 0),
("itself", 1), ("num", 0), ("int", 0), ("example", 0), ("atree", 2)]:
(string * int) list
See also
Theory.constants,
Theory.current_axioms,
Theory.current_definitions,
Theory.current_theorems,
Theory.new_type,
Definition.new_type_definition,
Theory.parents,
Theory.ancestry