[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable
c.sternagel at gmail.com
Thu Dec 5 17:17:23 CET 2013
sorry, I fail to understand both parts of your message ;)
First, I do not understand your justification why nothing is wrong.
Could you elaborate?
Second, are you saying that ad-hoc overloading should not be expanded on
rhss of abbreviations. If so, why? For me that does not sound desirable.
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev