define_type_raw : (hol_type * (string * hol_type list) list) list -> thm * thm
Like define_type but from a more structured representation than a string.
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
- FAILURE CONDITIONS
May fail for the usual reasons define_type may.
Not intended for general use, but sometimes useful in proof tools that want to
generate inductive types.
- SEE ALSO