----------------------------------------------------------------------
mk_bool_case                                              (boolSyntax)
----------------------------------------------------------------------
mk_bool_case : term * term * term -> term

SYNOPSIS
Constructs a case expression over {bool}.

DESCRIBE
{mk_bool_case M1 M2 b} returns {bool_case M1 M2 b}. The prettyprinter
displays this as {case b of T -> M1 || F -> M2}. The {bool_case} constant
may be thought of as a pattern-matching version of the conditional.

FAILURE
Fails if {b} is not of type {bool}. Also fails if {M1} and {M2} do not
have the same type.

EXAMPLE

- mk_bool_case (Term`f x`,Term`b:'b`,Term`x:bool`);
<<HOL message: inventing new type variable names: 'a, 'b>>

> val it = `case x of T -> f x || F -> b` : term




SEEALSO
boolSyntax.dest_bool_case, boolSyntax.is_bool_case.

----------------------------------------------------------------------