dest_eq : term -> term * term

SYNOPSIS

Term destructor for equality.

DESCRIPTION

dest_eq(`t1 = t2`) returns (`t1`,`t2`).

FAILURE CONDITIONS

Fails with dest_eq if term is not an equality.

EXAMPLE

  # dest_eq `2 + 2 = 4`;;
  val it : term * term = (`2 + 2`, `4`)

SEE ALSO

is_eq, mk_eq.