[Agda] class inheritance

Nils Anders Danielsson nad at chalmers.se
Fri Aug 10 23:11:19 CEST 2012

On 2012-08-10 21:06, Serge D. Mechveliani wrote:
> this is on inheritance of `classes' (records), in Agda and in
> Standarad library (lib-0.6).

The approach used in the library (sharing by parametrisation, or
Pebble-style sharing) is documented in the README. There are other
approaches, see for instance Randy Pollack's "Dependently Typed Records
in Type Theory", which I have mentioned before on this list:

   Re: Avoiding implicit argument proliferation?


More information about the Agda mailing list