dest_cond : term -> term * (term * term)

SYNOPSIS

Breaks apart a conditional into the three terms involved.

DESCRIPTION

dest_cond is a term destructor for conditionals:

   dest_cond `if t then t1 else t2`

returns (`t`,`t1`,`t2`).

FAILURE CONDITIONS

Fails with dest_cond if term is not a conditional.

SEE ALSO

mk_cond, is_cond.