[isabelle] problem with class and sulocale declarations
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] problem with class and sulocale declarations
- From: Viorel Preoteasa <viorel.preoteasa at abo.fi>
- Date: Wed, 08 Sep 2010 10:08:39 +0300
- User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:188.8.131.52) Gecko/20100802 Thunderbird/3.1.2
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and