mk_cond : term * term * term -> term
SYNOPSIS
Constructs a conditional term.
DESCRIPTION
mk_cond(`t`,`t1`,`t2`)
returns
`if t then t1 else t2`
.
FAILURE CONDITIONS
Fails with
mk_cond
if
t
is not of type
`:bool`
or if
t1
and
t2
are of different types.
SEE ALSO
dest_cond
,
is_cond
.