Hi Michael,
Thanks very much, I'll take your solution.
Regards,
Chun
On 24 April 2017 at 01:42, <michael.norr...@data61.csiro.au> wrote:
> 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
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
