[isabelle-dev] Type variables differing only in sort constraint
makarius at sketis.net
Thu May 27 11:10:42 CEST 2010
On Thu, 27 May 2010, Florian Haftmann wrote:
> It is possible to enter type variables distinguished only by sort
> constraint on the Isar level:
> assumes "P TYPE('a::order)" and "Q TYPE('a::group_add)"
> shows "R TYPE('a::power)"
> using assms proof -
> It is not clear to me whether this his always been possible that way or
> slipped in due to some change.
While this is OK for the low-level inference kernel, the syntax layer is
supposed to prevent such inconsistent constraints (both for type and term
The above is accepted even in Isabelle2005, and nobody has noticed so far.
When introducing the present check/uncheck infrastructure some years ago I
did notice some internal oddities concerning sort constraints that are
probably responsible for this effect. Some weeks ago I actually managed
to clear out some part of it (sort constraints for type specifications),
but did not get to the bottom of the whole syntax stack.
After the next round of check/uncheck modernization it should work in the
intended strict sense.
More information about the isabelle-dev