dest_arb : term -> hol_type
STRUCTURE
boolSyntax
SYNOPSIS
Extract the type of an instance of the
ARB
constant.
LIBRARY
DESCRIPTION
If
M
is an instance of the constant
ARB
with type
ty
, then
dest_arb M
equals
ty
.
FAILURE
Fails if
M
is not an instance of
ARB
.
COMMENTS
When it succeeds, an invocation of
dest_arb
is equivalent to
type_of
.
SEEALSO
mk_arb
,
is_arb
HOL
Kananaskis-13