[isabelle-dev] internal TYPE exception at lemma statement
makarius at sketis.net
Tue Nov 2 14:46:39 CET 2010
On Mon, 4 Oct 2010, Alexander Krauss wrote:
> To avoid that this issue, encountered by Lars, gets lost, I'll re-raise it
> The following lemma statement raises an obscure internal TYPE exception:
> assumes "P foo" (is "P ?bar")
> shows "Q ?bar"
> I assume that is-bindings cannot be used in the same structured statement. I
> also assume that this would be hard to support in general.
Yes, allowing to bind and reference within the same "expression" would
mean to have full Hindley-Milner let-polymorphism there. This was
dismissed as too complicated in the 2nd generation locale implementation
around 2001/2002, and in the current 3rd or 4th generation it is probably
not easier to achieve that. (Our type inference framework does not even
have a notion of truely local polymorphism.)
At some point, the error behaviour could be improved, though.
Technically it is a bit related to the surprise concerning ?thesis in
'interpretation' noticed by Brian Huffman recently: the simplistic
treatment of 'is' patterns in Isar proof commands is stretched a bit too
far by these more complex applications.
More information about the isabelle-dev