\DOC binders

\TYPE {binders : (string -> term list)}

\SYNOPSIS
Lists the binders in the named theory.

\DESCRIBE
The function {binders} 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 binders
declared in the named theory.

\FAILURE
Fails unless the given theory is an ancestor of the current theory.

\EXAMPLE
{
#binders `bool`;;
["$?!"; "$!"; "$@"] : term list

#binders `ind`;;
[] : term list
}
\SEEALSO
ancestors, axioms, constants, definitions, infixes, new_binder, parents, types.

\ENDDOC