mk_cond
boolSyntax.mk_cond : term * term * term -> term
Constructs a conditional term.
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.