Like define_type but from a more structured representation than a string.
DESCRIPTION
The core functionality of define_type_raw is the same as define_type, but
the input is a more structured format for the type specification. In fact,
define_type is just the composition of define_type_raw and
parse_inductive_type_specification.
FAILURE CONDITIONS
May fail for the usual reasons define_type may.
USES
Not intended for general use, but sometimes useful in proof tools that want to
generate inductive types.