Re: [isabelle] Variable 'b::{} not of sort type

On Thu, 1 Nov 2012, Gerwin Klein wrote:

Lars politely didn't point out my lame Google skills and sent me this link: at

I guess the conclusion is, we stick with the workaround. I hope my email had enough additional keywords in it to make this show up in searches more easily.

The main keywords are "Strugatsky" and "Stalker" :-)

Skimming over the thread cited above of this recurrent Isabelle type class topic, I take it as a reminder to improve the PIDE document feedback about results of type-inference (in Isabelle/jEdit only, not Proof General / TTY anymore). Then users will see better what type-inference has produced for them, with extra markup for freshly introduced types and their sorts.

Until this happens (not before the coming release), I recommend to read the book, such that the jokes and allusions about the "Zone" become easier to understand. See also


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.