[isabelle-dev] adhoc overloading: order inserting overloaded constant
makarius at sketis.net
Sat Feb 1 20:35:01 CET 2014
On Sat, 1 Feb 2014, Christian Sternagel wrote:
> So my idea was to instead use top-down rewriting (i.e., first replace
> maximal subterms that fit a given pattern). This is what
> "Pattern.rewrite_term_top" does, right? So after replacing
> "rewrite_term" by "rewrite_term_top", I get the expected results.
> Now my question. Can anybody think of a reason why "rewrite_term_top"
> would not be generally preferable over "rewrite_term" inside of
This is an old story. Printing usually works better top-down, e.g. see
good old 'translations' with their yo-yo strategy. When 'abbreviation'
was introduced, there was Pattern.rewrite_term, but not
Pattern.rewrite_term_top yet, so there was no other way.
I kept telling Stefan Berghofer about that omission until he made an
laternative version in 2010: see 6e45e4c94751, 5d2fe4e09354 (with typical
tell-nothing log entries).
So in analogy, the same will probably work for adhoc_overloading as well,
without going through all the reasoning again.
> If not, could one of the devs incorporate this tiny change please?
OK, I will try this out.
More information about the isabelle-dev