> Is this a regression in the type inference of locale expressions, or has it > always (i.e. since 2009) been like this?
I did not check this yet, but it is very likely that this has been
undetected since ever. I will figure out…
Florian
>
> Clemens
>
>
> On 04 September, 2014 09:21 CEST, Florian Haftmann
> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>
>> At d6a2e3567f95, I am currently analysing a problem with type inference
>> in locale expressions: when leaving types implicit, imported parameters
>> are given disjoint types despite they could be unified, and are so if
>> given explicit type annotations. The problem occurs if the imported
>> locales themselves have dependencies on other locales containing a
>> definition.
>>
>> The reason why this is really annyoing is that it breaks certain class
>> specifications to typecheck and currently effectively prevents me from
>> adding such a simple thing as product over lists.
>>
>> See attached theory for quite minimal examples.
>>
>> I will have to investigate this further.
>>
>> Florian
>>
>> --
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
>
>
>
> _______________________________________________
> 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
