[Agda] Struggling with irrelevance

Nils Anders Danielsson nad at cse.gu.se
Wed Jan 22 17:36:39 CET 2020


On 2020-01-22 16:34, Mathijs Kwik wrote:
> Neither the manual nor the release notes make note of this facility.

It has not been released yet.

> Why not just make the default version in Data.Empty use irrelevance?

"Redefine Bottom to make use of Prop?"
https://github.com/agda/agda-stdlib/issues/645

-- 
/NAD


More information about the Agda mailing list