Hi all, I would like to add a pretty-printing rule to completely omit a constructor and only print its argument. (I understand this means the resulting output won't parse back to the same input without type inference help.) Is it possible to do this in any way short of making a userprinter?
To be concrete, I have the following: Datatype`mlstring = strlit (char list)` and I would like the printer to print "hello" rather than strlit "hello" in my HOL-munged LaTeX output. (Userprinters are very difficult to use with the munger, so I would like to avoid them if possible.) Cheers, Ramana
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
