Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

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.