Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Michael.Norrish
There’s certainly a bug here: I want the superscript T for relations and the superscript -1 for reals, and the two need not mix. I think there’s a straightforward enough solution that will allow “inv” to be used as an input method for both. Michael On 17/10/17, 06:57, "Chun Tian"

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Mario Castelán Castro
On 16/10/17 14:55, Chun Tian wrote: > I’m using HOL built from latest Git “master” branch; you’re using HOL > Kananaskis-11 release. Understood. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan signature.asc Description:

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Chun Tian
I’m using HOL built from latest Git “master” branch; you’re using HOL Kananaskis-11 release. —Chun > Il giorno 16 ott 2017, alle ore 17:01, Mario Castelán Castro > ha scritto: > > On 16/10/17 09:35, Chun Tian (binghe) wrote: >> I'm fine with constant overloading. But

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Mario Castelán Castro
On 16/10/17 09:35, Chun Tian (binghe) wrote: > 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

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Chun Tian (binghe)
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"

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Mario Castelán Castro
If you want to completely remove the mapping of “inv” to the constant from “realax”, then do “remove_ovl_mapping "inv" {Name = "inv", Thy = "realax"};”. This constant can then still be accessed with “realax$inv”. -- Do not eat animals; respect them as you respect people.

Re: [Hol-info] Conflicted "inv" pp_elements in relationTheory and realaxTheory

2017-10-16 Thread Mario Castelán Castro
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";