Hi, I have a simple data type based on strings:
val _ = Datatype `Label = name string | coname string`; Is is possible to set up pretty-printing (or gammar) rules, such that: 1. The term `` `a` `` can be interpreted as `` name “a” `` 2. The term`` -`a` `` can be interpreted as `` coname “a” `` I wanted to call add_rule() on term names “name” and “coname”, but I see no way to remove the outside double-quotes (“) from the string being printed. P. S. I’m fine if the single-backquote (`) is replaced by other symbols if it’s not conflicted with major theories provided in HOL). Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
