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

See also

boolSyntax.dest_bool_case, boolSyntax.is_bool_case