See now http://isabelle.in.tum.de/reports/Isabelle/rev/7f990b3d5189
which seems to do the job. There a still dark corners wrt. to base sort
inference which maybe one day will lift its ugly head but for the moment
it is OK.
Florian
On 10.09.2014 10:35, Florian Haftmann wrote:
Hi
This is what I expected. Type inference of locale expressions is inherently
heuristic and probably you are hitting this. (This could be verified further
with a stack trace). For more background, see also this earlier message:
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
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
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
