[Agda] many ways to import the same thing from record

mechvel at scico.botik.ru mechvel at scico.botik.ru
Mon Jun 8 22:20:46 CEST 2020


On 2020-06-08 23:15, mechvel at scico.botik.ru wrote:
> 
> [..]
> 

> This is an approach to define Class, SubClasss, SubSubClass ...
> where  SubClass has Class as an argument.
> 

An important correction of a typo:

    IsSubClass has Class as an argument.

--
SM


More information about the Agda mailing list