# let th = ARITH_RULE `(\x. x < 32) 0`;;
val th : thm = |- (\x. x < 32) 0
# let absth,repth = new_basic_type_definition "32" ("mk_32","dest_32") th;;
val absth : thm = |- mk_32 (dest_32 a) = a
val repth : thm = |- (\x. x < 32) r <=> dest_32 (mk_32 r) = r
and here is a declaration of a type of finite sets over a base type,
a unary type constructor:
# let th = CONJUNCT1 FINITE_RULES;;
val th : thm = |- FINITE {}
# let tybij = new_basic_type_definition "fin" ("mk_fin","dest_fin") th;;
val tybij : thm * thm =
(|- mk_fin (dest_fin a) = a, |- FINITE r <=> dest_fin (mk_fin r) = r)
so now types like