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" <binghe.l...@gmail.com> wrote:
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
<marioxcc...@yandex.com> ha scritto:
>
> 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 "inv" for relations.
>
> I do not know what is your situation. In my case (HOL4 Kananaskis-11),
> there is no custom parser rule for relation$inv:
>
> “mario@svetlana [0] [/home/mario]
> $ hol
>
> ---------------------------------------------------------------------
> HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 06 16:33:32 2017)]
>
> For introductory HOL help, type: help "hol";
> To exit type <Control>-D
> ---------------------------------------------------------------------
>> ancestry "-";
> val it =
> ["ConseqConv", "quantHeuristics", "ind_type", "operator", "while",
> "pair",
> "num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
> "one", "marker", "combin", "min", "bool", "sat", "sum", "option",
> "basicSize", "numpair", "pred_set", "list", "rich_list"]: string list
>> “inv R”;
> <<HOL message: inventing new type variable names: 'a>>
> val it = ``inv R``: term”
>
> --
> 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
------------------------------------------------------------------------------
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
