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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
