datatype_thm_to_string

EmitTeX.datatype_thm_to_string : thm -> string

Converts a datatype theorem to a string.

An invocation of datatype_thm_to_string thm, where thm is a datatype theorem produced by Hol_datatype, will return a string that corresponds with the orginal datatype declaration.

Failure

Will fail if the supplied theorem is not a datatype theorem, as created by Hol_datatype.

Example

> new_theory "example";
<<HOL message: Restarting theory "example">>
<<HOL warning: Theory.callhooks: Hook Parse.clear_consts_from_grammar failed on event NewTheory{oldseg = "example", newseg = "example"} with problem 
Exception raised at Term.dest_thy_const: not a const
>>
val it = (): unit
> val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
> EmitTeX.datatype_thm_to_string (theorem "datatype_example");
val it = "example = First | Second": string

See also

bossLib.Hol_datatype