dest_var : term -> string * hol_type

SYNOPSIS

Breaks apart a variable into name and type.

DESCRIPTION

dest_var `var:ty` returns ("var",`:ty`).

FAILURE CONDITIONS

Fails with dest_var if term is not a variable.

EXAMPLE

  # dest_var `x:num`;;
  val it : string * hol_type = ("x", `:num`)

SEE ALSO

mk_var, is_var, dest_const, dest_comb, dest_abs, name_of.