Re: [isabelle] How to State Class Duality?
On Tue, 14 Dec 2010, Clemens Ballarin wrote:
There is yet another approach, explored by Makarius in an early
experiment in HOL/Lattice/Orders.thy. There the functor that maps the
structure to its dual is a type constructor, which is also lifted to the
term level. I believe this dates back to times when axclasses were the
tool of choice for such formalisations.
Yes, it dates back to my version of the standard type class examples from
the early times around 1992/1993. Back then Tobias had a TYPES talk that
claimed that functors over type classes would *not* work. So I included
the dual constructor as a positive example when my version of axclasses
became available in 1994.
This archive was generated by a fusion of
Pipermail (Mailman edition) and