Re: [isabelle] problem with class and sulocale declarations



 Hi Florian,

Your suggested solution is the first thing that I tried myself, however it did not help.
The problem occurs also for:

class bounded_some_algebra = zero + some_algebra

without assumptions.

Best regards,

Viorel

On 9/8/2010 10:30 AM, Florian Haftmann wrote:
Hi Viorel,

class bounded_some_algebra = zero + some_algebra +
   assumes zero_smallest: "0<= a"

However, when I introduce this declaration I get the error:

*** Type unification failed
***
*** Cannot meet type constraint:
***
*** Term:  times::'b =>  'b =>  'b :: 'b =>  'b =>  'b
*** Type:  'a =>  'a =>  'a
***
*** At command "class".
this problem has indeed already been detected and will disappear in the
next Isabelle release.  For the moment an explicit type annotation
should help:

class bounded_some_algebra = zero + some_algebra +
   assumes zero_smallest: "(0::'a)<= a"

Sorry for the inconvenience,
	Florian







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