mk_arb : hol_type -> term
STRUCTURE
boolSyntax
SYNOPSIS
Creates a type instance of the
ARB
constant.
LIBRARY
DESCRIPTION
For any HOL type
ty
,
mk_arb ty
creates a type instance of the
ARB
constant.
FAILURE
Never fails.
COMMENTS
ARB
is a constant of type
'a
. It is sometimes used for creating pseudo-partial functions.
SEEALSO
dest_arb
,
is_arb
,
arb
HOL
Kananaskis-14