*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Polymorphic minus*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 20 Sep 2011 12:16:10 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAP0k5J7mi7tiFGj_kiCySZHTsk9pczmFwVVfpdjmEPfe4nqjNg@mail.gmail.com>*References*: <CAP0k5J4KTqCs4jZvtyDHLTtRW-RoVzewgQyOeTa1XrRrczNMNg@mail.gmail.com> <FAC22F1B-2EA7-4F10-8573-D9B5A43EB9ED@uibk.ac.at> <CAP0k5J7mi7tiFGj_kiCySZHTsk9pczmFwVVfpdjmEPfe4nqjNg@mail.gmail.com>

> I see. But > > fixes a :: "'T :: minus" > > means that a is assigned to a type variable 'T rather than a concrete > type T. What if a is of a concrete type? Then this type T has to be in the class minus, otherwise you cannot write "a - a". René > 2011/9/20 René Thiemann <rene.thiemann at uibk.ac.at>: >>> If my understanding is correct, the minus operator has a polymorphic type: >>> 'a => 'a => bool. However, if I have something like: >> >> But 'a must have sort minus. >> >> I would start as follows >> >> locale test = >> fixes a :: "'T :: minus" >> assumes ax1: "a - a = a" >> begin -- René Thiemann mailto:rene.thiemann at uibk.ac.at Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-6434 University of Innsbruck

**References**:**[isabelle] Polymorphic minus***From:*John Munroe

**Re: [isabelle] Polymorphic minus***From:*René Thiemann

**Re: [isabelle] Polymorphic minus***From:*John Munroe

- Previous by Date: Re: [isabelle] Polymorphic minus
- Next by Date: [isabelle] Isabelle /HOL how to compile program
- Previous by Thread: Re: [isabelle] Polymorphic minus
- Next by Thread: [isabelle] Isabelle /HOL how to compile program
- Cl-isabelle-users September 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list