Re: [isabelle] using mono predicate
there is no direct way to enforce this. The easiest is to add a trivial
assumption which introduces the sort constraint, for example:
class test = lattices +
assumes "(a :: 'a :: order) = a"
The class command also accepts the constrains element that locales support, but
this seems to be without effect.
Viorel Preoteasa schrieb:
Thank you for your answer. I have figured out the problem myself and
I solved it by adding my definition of monoa in the context of class test.
I have anyway a question. How do I implement point 2 from your suggested
On 4/28/2011 2:51 PM, Andreas Lochbihler wrote:
2. Change the definition of class test such that 'a has the sort
constraint order. The conditions are similar to 1., but now,
everything in context test includes the sort constraint.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 023
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and