[isabelle-dev] Pending sort hypotheses

[Amine Chaieb]

OK, I see now that buried somewhere in Abstract_Rat old unconstrained
rewrites have a new assupmtion


  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


That might explain some of the bahaviour.


Amine.


Amine Chaieb wrote:

> Dear all,
>
>
> I am having problems with updating a theory, which used to work by the
> end of last year.
>
>
> Now I get at some point the following error: 
>
> Pending sort hypotheses: {ring_char_0,division_by_zero,field}
>
>
> after simp has succeeded to solve the goal.
>
>
> The problem is that none of by Hypotheses, assumptions or goal depend on
> these sorts!!
>
>
> I have tried to trace the simplifier (I had also a strange experience
> here, even when I set the trace depth limit to 1000000 I still get a
> broken trace at the same places with limit roughly 1000). In the over
> 68K lines of trace there is no mention of any type 'a with those sorts.
>
>
> The proof used to by one line (by simp).
>
>
> Anybody knows how to explain this behaviour?
>
>
> Best wishes,
>
> Amine.
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>