mk_arb

boolSyntax.mk_arb : hol_type -> term

Creates a type instance of the ARB constant.

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.

See also

boolSyntax.dest_arb, boolSyntax.is_arb, boolSyntax.arb