mk_eq : term * term -> term

SYNOPSIS

Constructs an equation.

DESCRIPTION

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

FAILURE CONDITIONS

Fails with mk_eq if t1 and t2 have different types.

EXAMPLE

  # mk_eq(`1`,`2`);;
  val it : term = `1 = 2`

SEE ALSO

dest_eq, is_eq.