Am 28.01.2015 um 13:37 schrieb Christian Sternagel: > During a visit of Florian in Innsbruck we had some discussion on adhoc > overloading. One suspicion was that schematic type variables from > variants had to be "paramified" before using the resulting type unifier. > > I tried to do so in the attached patch. Unfortunately, I still obtain > the following error in > > ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy > > Illegal schematic type variable: ?'a2 > > Please let me know if you have any comments on this topic (especially on > what is going on in the function "unify_filter").
The idea was to imitate how regular constants are handled by type
inference. I am not sure whether I interpreted the sources right during
our session, and I did not have a close look at the patch either.
Beside that, the same applies as mentioned in my previous post on ad-hoc
overloading.
All the best,
Florian
>
> cheers
>
> chris
>
> On 01/20/2015 06:16 PM, Makarius wrote:
>> On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
>>
>>>> Just a reminder that this old thread is not yet resolved and
>>>> currently I'm essentially stuck.
>>>
>>> I hope somebody who has a clue will answer your email.
>>
>> I still have various "important" markers on this mail thread, to see if
>> I can tell something about it, but I did not manage to pick it up again.
>> It will happen really soon now ...
>>
>>
>>>> drop_semicolons
>>>
>>> I’ve applied and push your first change.
>>>
>>> As for semicolon, the standard style is rather to put them, not to
>>> drop them.
>>
>> Strictly speaking there is no standard for semicolons in Isabelle/ML,
>> only the universal standard of uniformity: a file either has extra
>> semicolons or does not have extra semicolons.
>>
>>
>> More than 20 years ago, semicolons where generally en-vogue, and no
>> surprise for me in SML. Then they became less popular, e.g. in Scala we
>> now see sophisticated rules for implicit "semicolon inference". The
>> Isar language has lost its semicolon altogether some weeks ago
>> (5ff61774df11).
>>
>> Over the decades I have occasionally experimented with writing less
>> semicolons in ML, but each time I ran into practical inconveniences
>> concerning error situations (broken partial input), and closed ML
>> modules versus open sequences of declarations (e.g. in the 'ML' command).
>>
>> My present style of doing it (approx. the last 10 years) is somehow
>> optimized in that respect. Whenever I do serious renovations on some
>> old ML module, I first normalize the semicolon style (and other styles
>> as well), just to save a lot of time in the actual work.
>>
>>
>> Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
