mk_cond : term * term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Constructs a conditional term.
DESCRIPTION
mk_cond(t,t1,t2)
constructs an application
COND t t1 t2
. This is rendered by the prettyprinter as
if t then t1 else t2
.
FAILURE
Fails if
t
is not of type
bool
or if
t2
and
t2
are of different types.
COMMENTS
The prettyprinter can be trained to print
if t then t1 else t2
as
t => t1 | t2
.
SEEALSO
dest_cond
,
is_cond
HOL
Kananaskis-13