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