HOL's pretty-printer usually prints the empty list as "[]", which I believe
is produced by two separate tokens (one for each bracket) via a "listform"
parsing/printing rule.
In LaTeX math mode (generated using HOL's math mode munger) "[]" does not
look nice: it needs a bit of space inside. What would be the best approach
to making the printer generate such space? Could I, perhaps, override the
empty list (but not other lists) with a special token that I can then
override to some custom LaTeX? Or perhaps there's a better way?
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
