Email Gateway (Aug 18 2022 at 11:07): Email Gateway (Aug 18 2022 at 11:07):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 08:18 UTC