On 05/27/2013 05:26 PM, Makarius wrote:
Anyway, after 2-3 more rounds of investigation, I've found more profound
weaknesses of pattern.ML and unify.ML concerning unification of types. This
could lead to situations as sketched above, where types of variables were not
properly instantiated. E.g. here:
[...]
The following change addresses that, although I do not claim to "fix" anything
-- it is even more critical as usual, since it affects operations of the inference kernel.
Hi Markus,
I do not quite understand the rationale behind this change. As I pointed out in
my previous mail,
it is an error to supply disagreement pairs to unify containing Vars that have
the same name but
different types. So I don't think one should change pattern.ML and unify.ML so
that it unifies
these different types and pretends that everything is all right, but one should
find and correct
the function that supplies these erroneous disagreement pairs to unify. Do we
have an idea where
these disagreement pairs came from? Maybe someone just forgot to increment the
indices of variables
before invoking bicompose?
Greetings,
Stefan
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
