Is this a regression in the type inference of locale expressions, or has it always (i.e. since 2009) been like this?
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
