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

[Florian Haftmann]

Hi Christian,

>> 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.
> Does that also mean that the resulting "unit itself" is as you would
> expect in the following?
> 
>   abbreviation
>     "abbr2 == do {
>       Some ();
>       Some False
>     }" -- "additional type variable"

I would say so.

> By "expanding adhoc overloading" do you mean replacing concrete
> constants by overloaded generic ones?

Yes.

> When is Proof_Context.abbrev_mode actually true?

When parsing abbreviation declarations.

> What I first thought was that I should avoid to insert overloaded (i.e.,
> generic constants; cf. Adhoc_overloading.insert_overloaded) constants
> whenever Proof_Context.abbrev_mode is true. But just trying this on some
> examples did not change anything (as far as I can tell).

Did your examples interleave abbreviations and syntactic ad-hoc
overloading?  Only then effects are about to be expected.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140208/9f88214e/attachment.sig>