*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] problem with class and sulocale declarations*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Wed, 08 Sep 2010 10:54:21 +0300*In-reply-to*: <4C873BA2.6030603@informatik.tu-muenchen.de>*References*: <4C873677.6010001@abo.fi> <4C873BA2.6030603@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

Hi Florian,

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

**References**:**[isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] problem with class and sulocale declarations
- Next by Date: Re: [isabelle] Congruence rule for Let
- Previous by Thread: Re: [isabelle] problem with class and sulocale declarations
- Next by Thread: Re: [isabelle] problem with class and sulocale declarations
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list