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 MHonArc.