The grammar is determined in the same way as when grammars are merged by the
action of loading a bunch of ancestor theories. The safest way to disable reln
in your situation would probably to have a theory that removes the abbreviation
and then is the only thing loaded by the munger. (How do you know with your
ppLib approach that ppLib is the last thing to be loaded?)
I've added test-cases to src/TeX/theory_tests (see commit 29db124) indicating
that scenarios like yours seem to be behaving as expected.
Michael
On 06/03/15 05:33, Ramana Kumar wrote:
> I'm having a lot of trouble trying to remove a type abbreviation when using
> the
> HOL->TeX munger. I make the munger with a main theory that calls
> Parse.disable_tyabbrev_printing "reln". And if I load this theory in an
> interactive HOL session and type ``:'a -> 'a -> bool`` it prints back as I
> expect. But if I use \HOLty{:'a -> 'a -> bool} in my LaTeX document and run it
> through the munger, it prints as "'a reln" in the resulting tex file.
>
> I've also tried making the munger with a ppLib.sml that explicitly sets the
> type
> grammar to something that does not include "reln" (using
> type_grammar.remove_abbreviation), but it still appears in the output! How
> does
> the grammar for the munger get determined?
>
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming The Go Parallel Website, sponsored
> by Intel and developed in partnership with Slashdot Media, is your hub for all
> things parallel software development, from weekly thought leadership blogs to
> news, videos, case studies, tutorials and more. Take a look and join the
> conversation now. http://goparallel.sourceforge.net/
>
>
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
