Hi,
In relationTheory there's a "inv" operatior for inverting a relation:
(* ----------------------------------------------------------------------
inverting a relation
---------------------------------------------------------------------- *)
val inv_DEF = new_definition(
"inv_DEF",
``inv (R:'a->'b->bool) x y = R y x``);
(* superscript suffix T, for "transpose" *)
val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
fixity = Suffix 2100,
paren_style = OnlyIfNecessary,
pp_elements = [TOK (UTF8.chr 0x1D40)],
term_name = "inv"}
while there's another rule in realaxTheory, setting it differently:
val _ =
add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
fixity = Suffix 2100,
paren_style = OnlyIfNecessary,
pp_elements = [TOK (UnicodeChars.sup_minus ^
UnicodeChars.sup_1)],
term_name = "inv"}
As a result, when I start HOL (in which relationTheory is loaded by
default), I see the "transpose" representation of ``inv R``:
---------------------------------------------------------------------
HOL-4 [Kananaskis 11 (expknl, built Mon Oct 16 12:19:37 2017)]
For introductory HOL help, type: help "hol";
To exit type <Control>-D
---------------------------------------------------------------------
> ``inv R``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = “Rᵀ”: term
But after loading realTheory (directly or indirectly), it permanently
becomes $R^{-1}$:
> load "realTheory";
val it = (): unit
> ``inv R``;
<<HOL message: more than one resolution of overloading was possible>>
val it = “R⁻¹”: term
> ``inv (R :'a -> 'a -> bool)``;
val it = “R⁻¹”: term
Further more, their TeX notations were never defined, thus in TeX-based PDF
it simply shows "inv R".
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.
Regards,
Chun Tian
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
