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

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] line wrap length in hol-mode

On 16/10/17 17:15, michael.norr...@data61.csiro.au wrote: > You need to adjust Globals.linewidth (an int ref). Thanks. -- 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

Re: [Hol-info] line wrap length in hol-mode

You need to adjust Globals.linewidth (an int ref). Michael On 17/10/17, 03:57, "Mario Castelán Castro" wrote: Hello. How can I change the column at which the pretty printer will wrap expressions using hol-mode in GNU Emacs? I want it to use the full width of

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

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

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

[Hol-info] line wrap length in hol-mode

Hello. How can I change the column at which the pretty printer will wrap expressions using hol-mode in GNU Emacs? I want it to use the full width of the Emacs “window” (the cell that displays a buffer, not the whole window). -- Do not eat animals; respect them as you respect people.

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

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

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

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

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

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

Hi, In relationTheory there's a "inv" operatior for inverting a relation: (* -- inverting a relation -- *) val inv_DEF = new_definition( "inv_DEF",

Re: [Hol-info] Converting ordinals from different type variables?

Hi Michael, Thanks very much, this saves me lots of time trying to prove something impossible. Regards, Chun Tian On 16 October 2017 at 00:59, wrote: > The definition is fine, but will not have the nice properties you want > (e.g., monotonicity) if the