[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable
florian.haftmann at informatik.tu-muenchen.de
Thu Dec 5 17:05:20 CET 2013
Reviving this old thread, Peter and me found out what is actually going
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode). @Christian. You might consider to adjust
your code accordingly after a second round of thinking about.
On 13.10.2013 17:36, Florian Haftmann wrote:
>>> Here a bisect would be helpful when this came to happen
>>> actually (or is it already present in Isabelle2013).
>> This one already goes wrong in Isabelle2013.
> OK. I guess it is some variant of the ever recurring problem of »hidden
> polymorphism«. Will take some time to figure out actually.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev