To reconstruct the datatype you can use EmitTeX.datatype_thm_to_string, which is documented.
Anthony On 22 Mar 2012, at 09:14, Michael Norrish wrote: > Unfortunately there isn't any documentation for emitLib. If you figure > anything out, patches fixing this situation would be gratefully received. > There are a number of examples of probably useful uses of emitLib in the HOL > sources. If you figure out who wrote those calls (git blame may help), feel > free to hassle those people for enlightenment. Indeed, those people may well > be in your building. > > Michael > > On 22/03/2012, at 19:58, Ramana Kumar <[email protected]> wrote: > >> Is EmitML documented somewhere? I don't think I saw it in the Description >> manual. >> In particular, I'm wondering whether I need to repeat the quotation of a >> datatype for EmitML.DATATYPE (after having passed it once already to >> Hol_datatype) if I want to emit a datatype, or whether it can be >> reconstructed somehow based on whatever Hol_datatype stores. > ------------------------------------------------------------------------------ This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
