mk_bool_case : term * term * term -> term
STRUCTURE
SYNOPSIS
Constructs a case expression over bool.
DESCRIPTION
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
HOL  Trindemossen-1