I'm fine with constant overloading. But I think the "term_name" used in
add_rule() doesn't know constant overloading at all. After realaxTheory is
loaded, the previous rule defined in relationTheory has absolutely no
effects, even I'm using "inv" for relations.
But I don't mind if relation "inv" also uses "^{-1}" (so we should move the
rule from realaxTheory to relationTheory and remove the existing one in
relationTheory).
---
Chun
On 16 October 2017 at 16:02, Mario Castelán Castro <marioxcc...@yandex.com>
wrote:
> 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
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
