Re: [isabelle] using mono predicate

Hello Viorel,

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:
Hello Andreas,

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 solutions?

Best regards,


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
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
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 MHonArc.