Email Gateway (Aug 19 2022 at 10:38): Email Gateway (Aug 19 2022 at 10:38):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jesus,
More generally, is there a difference between the two following type
class definitions? Is there a "better" or a "more appropriate" way to
proceed?
class A = bar +
fixes foo :: "'a::type"class B =
fixes foo :: "'a::bar"
Definitely. For class A, you get at the back a locale A importing from
another locale bar, with a corresponding type class A which is a
subclass of another type class bar.
For class B, you get at the back a locale B which does not import any
other locale, with a corresponding type class B which is a subclass of
another type class bar.
For class A, you can prove additional locale dependencies plus
corresponding subclass relations by means of subclass.
For class B, you can only prove additional subclass relations by means
of instance … \<subseteq> …, in lack of a corresponding locale for the
potential superclass.
I would suggest to go the path with classes of shape A unless there are
good reasons not to do so.
Cheers,
Florian
signature.asc
Last updated: Apr 25 2024 at 16:19 UTC