mk_bool_case
boolSyntax.mk_bool_case : term * term * term -> term
Constructs a case expression over bool.
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`);
val it = “if x then f x else b”: term