[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable

Florian Haftmann 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
on here.

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.
> 	Florian
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131205/587ef686/attachment.asc>

More information about the isabelle-dev mailing list