There’s no great way to do this at the moment, because it’s not possible to
have all the things that are possible inside string literals (e.g., \n) appear
in other contexts. My inclination would be overload n to name, and to overload
unary negation to coname, and then you could write
n"a" and -"a"
Michael
On 24/4/17, 02:15, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
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
------------------------------------------------------------------------------
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
