mk_disj : term * term -> term

SYNOPSIS

Constructs a disjunction.

DESCRIPTION

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

FAILURE CONDITIONS

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

EXAMPLE

  # mk_disj(`x = 1`,`y <= 2`);;
  val it : term = `x = 1 \/ y <= 2`

SEE ALSO

dest_disj, is_disj, list_mk_disj.