decls

Type.decls : string -> {Thy : string, Tyop : string} list

Lists all theories a named type operator is declared in.

An invocation Type.decls s finds all theories in the ancestry of the current theory with a type constant having the given name.

Failure

Never fails.

Example

> Type.decls "prod";
val it = [{Thy = "pair", Tyop = "prod"}]: {Thy: string, Tyop: string} list

Comments

There is also a function Term.decls that performs a similar operation on term constants.

See also

Theory.ancestry, Term.decls, Theory.constants