Re: [isabelle] Classes with two type variables?



Dear David,

> Am I correct to assume that classes  can only use one type variable?

Yes.  This is a fundamental property of the underlying logical calculus.

> Am I correct to assume that if I can define this as a  class, rather
> than a locale, it will make it easier to define theories as an instance
> of the general abstract theory?

Yes.  Locales have to be instantiated by means of interpretation,
whereas for type classes this is mostly implicit due to type inference.

> So is there some way to do this or would it be better to stay with  locales?

Since you need more than one type variables, it is better to stay with
locales.

Hope this helps
Florian

begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.