dest_const : term -> string * hol_type

SYNOPSIS

Breaks apart a constant into name and type.

DESCRIPTION

dest_const is a term destructor for constants:

   dest_const `const:ty`

returns ("const",`:ty`).

FAILURE CONDITIONS

Fails with dest_const if term is not a constant.

EXAMPLE

  # dest_const `T`;;
  val it : string * hol_type = ("T", `:bool`)

SEE ALSO