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
