types : string -> (string * int) list
STRUCTURE
Theory
SYNOPSIS
Lists the types in the named theory.
DESCRIPTION
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 =
    [("one", 0), ("option", 1), ("prod", 2), ("sum", 2),
     ("fun", 2), ("ind", 0), ("bool", 0), ("num", 0),
     ("recspace", 1), ("list", 1)] : (string * int) list
SEEALSO
constants, current_axioms, current_definitions, current_theorems, new_type, new_type_definition, parents, ancestry
HOL  Kananaskis-14