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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to