Thanks for the reply. I managed to fix my problem by going back through all
the ancestor theories under my control and removing the "reln" abbreviation
from the type grammar.
This was perhaps overkill, but worked. It's possible that conflicting
entries for the abbreviation was part of the problem (set_relation defines
it differently from wot and toto).
On Fri, Mar 6, 2015 at 3:31 AM, Michael Norrish <
[email protected]> wrote:
> 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
>
------------------------------------------------------------------------------
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
