On 18 Jan 2011, at 14:40, Roger Bishop Jones wrote: > I am finding that if I give something the status of a binder > before defining the constant, so that it can be used as a > binder in the definition, the definition fails. > > The error message alleges that the binder occurs freely in > the definition (which I suppose is true). > > Is this a known feature?
It is due to a bug in type inference that I fixed some time ago, but my plans for an OpenProofPower release in the second half of 2010 went awry. I plan a release including all the outstanding bug fixes and one or two minor new features before the end of January. Regards, Rob. > > Roger Jones > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
