Re: [isabelle] problem with class and sulocale declarations



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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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