dest_const

Term.dest_const : term -> string * hol_type

Breaks apart a constant into name and type.

dest_const is a term destructor for constants. If M is a constant with name c and type ty, then dest_const M returns (c,ty).

Failure

Fails if M is not a constant.

Comments

In Hol98, constants also carry the theory they are declared in. A more precise and robust way to analyze a constant is with dest_thy_const.

See also

Term.mk_const, Term.mk_thy_const, Term.dest_thy_const, Term.is_const, Term.dest_abs, Term.dest_comb, Term.dest_var