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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
