Hi Christian, > Thanks for pointing this out. While yours is a valid observation, it > seems that observing "abbrev_mode" is not enough to obtain nicer output, > i.e., when using > > fun uncheck ctxt ts = > - if Config.get ctxt show_variants orelse exists (is_none o try > Term.type_of) ts then ts > + if Proof_Context.abbrev_mode ctxt orelse > + Config.get ctxt show_variants orelse > + exists (not o can Term.type_of) ts then ts > else map (insert_overloaded ctxt) ts; > > instead of the above, the output of > > term "xs ≤⇩♯ ys" > > stays the same as in my initial post, namely > > "Foo.le_sharp ♯ xs ys"
i.e. the problem is still open, although the formal gap between
abbreviations and ad-hoc overloading got closer.
I have this issue on my agenda, though not prioritized. The
abbreviation machinery is a delicate issue, and so is the (un)check
machinery: it is not compositional, and additions are supposed to work
smoothly with all pre-existing plugins here.
In similar situations in the past I always did some phyiscal experiments
to get some clues what to examine next. The idea is to plug in an
(un)checker which does nothing than diagnostic output. Feeding this
with terms can give valid inspirations. A tedious issue, of course.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
