[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses
lp15 at cam.ac.uk
Fri Jul 6 15:27:46 CEST 2012
Thanks for investigating. Although he made a mistake, of course, we should deliver an intelligible error message and not simply allow an exception to propagate.
On 6 Jul 2012, at 13:56, Makarius wrote:
> On Tue, 3 Jul 2012, Lawrence Paulson wrote:
>> Does anybody know (without going to the trouble of reproducing this exact proof and obtaining a backtrace) why the function dest_equals is being called on a sort constraint? At a guess, something is expecting a definition.
> Henri had put the SORT_CONSTRAINT in the 'where' part of 'interpretation' and that expects a proper equation at some point. This is also explained in the manuals (isar-ref, locales).
> The confusion was coming from https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-July/msg00003.html where it looked like problem was solved.
> In most practical situations, SORT_CONSTRAINT as it is now (Isabelle2012 or today's Isabelle/3155cee13c49) works best in assumptions.
More information about the isabelle-dev