On 16/10/17 08:23, Chun Tian (binghe) wrote: > Is this something can be fixed? (I don't know how) i.e. preserving the > pp_setting of "inv" for relations and correctly define TeX notations for > both of them.
“inv” has 2 possible resolutions after loading realTheory:
> overload_info_for "inv";
inv parses to:
realax$inv
(relation$inv :(α -> α -> bool) -> α -> α -> bool)
inv might be printed from:
(relation$inv :(α -> α -> bool) -> α -> α -> bool)
realax$inv
val it = (): unit
Typically the correct one will be chosen by the parser because of type
constraints. If you want to force one of them, you can write
“relation$inv” or “realax$inv”. If you want to make the one from
“relation” the default, then do “overload_on("inv",“relation$inv”):”. I
do not know how to manipulate the TeX mapping.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
