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.

Andreas

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,

Viorel

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.edu
http://pp.info.uni-karlsruhe.de
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.