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
Class_Clash.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
