dest_bool_case : term -> term * term * term
STRUCTURE
boolSyntax
SYNOPSIS
Destructs a case expression over
bool
.
DESCRIPTION
If
M
has the form
bool_case M1 M2 b
, then
dest_bool_case M
returns
M1,M2,b
.
FAILURE
Fails if
M
is not a full application of the
bool_case
constant.
SEEALSO
mk_bool_case
,
is_bool_case
HOL
Kananaskis-14