datatype_thm_to_string : thm -> string
STRUCTURE
EmitTeX
SYNOPSIS
Converts a datatype theorem to a string.
DESCRIPTION
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: Created theory "example">>
> 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
SEEALSO
Hol_datatype
HOL  Kananaskis-14