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