[isabelle] problem with class and sulocale declarations



 Hello,

I have many algebraic structures developed as classes. At some point
I want a new class with additional constant zero.

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 occur after the sublocale declaration:

sublocale some_algebra < lattice1!:some_lattice_b "1" "op *" "op l->" "op <=" "op <" "op r->" "op ­\<squnion>1"

Here both some_lattice_b and some_algebra are subclasses of a common class.

If I introduce the class bounded_some_algebra before the sublocale, then it works,
except that I get a similar problem later when using bounded_some_algebra.

I tried to make a smaller example to show the problem, but I could not reproduce
it.

Best regards,

Viorel Preoteasa






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