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:

http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg01573.html

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 http://en.wikipedia.org/wiki/Roadside_Picnic


	Makarius






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