dest_thy_const
Term.dest_thy_const : term -> {Thy:string, Name:string, Ty:hol_type}
Breaks apart a constant into name, theory, and type.
dest_thy_const is a term destructor for constants. If M is a
constant, declared in theory Thy with name Name, having type ty,
then dest_thy_const M returns {Thy, Name, Ty}, where Ty is equal
to ty.
Failure
Fails if M is not a constant.
Comments
A more precise alternative to dest_const.
See also
Term.mk_const,
Term.dest_thy_const,
Term.is_const, Term.dest_abs,
Term.dest_comb, Term.dest_var