[isabelle-dev] Problem with type inference in locale expressions

2014-09-04 Thread Florian Haftmann
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

Re: [isabelle-dev] Problem with type inference in locale expressions

2014-09-04 Thread Clemens Ballarin
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

Re: [isabelle-dev] Problem with type inference in locale expressions

2014-09-04 Thread Florian Haftmann
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