mk_conj : term * term -> term

SYNOPSIS

Constructs a conjunction.

DESCRIPTION

mk_conj(`t1`,`t2`) returns `t1 /\ t2`.

FAILURE CONDITIONS

Fails with mk_conj if either t1 or t2 are not of type `:bool`.

EXAMPLE

  # mk_conj(`1 + 1 = 2`,`2 + 2 = 4`);;
  val it : term = `1 + 1 = 2 /\ 2 + 2 = 4`

SEE ALSO

dest_conj, is_conj, list_mk_conj.