decls

Term.decls : string -> term list

Returns a list of constants having the same name.

An invocation Term.decls s returns a list of constants found in the current theory having the name s. If there are no constants with name s, then the empty list is returned.

Failure

Never fails.

Example

> decls "+";
val it = [“$+”]: term list

> map dest_thy_const it;
val it = [{Name = "+", Thy = "arithmetic", Ty = “:num -> num -> num”}]:
   {Name: string, Thy: string, Ty: hol_type} list

Comments

Useful for untangling confusion arising from overloading and also the possibility to declare two different constants with the same name in different theories.

See also

Type.decls, Term.dest_thy_const