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"
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:
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
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
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"
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.
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";