[Agda] irrelevant contradiction?

[Apostolis Xekoukoulotakis]

Yes, in the agda-stdlib.
<https://github.com/agda/agda-stdlib/blob/64c90354189b9d497310197cccb989d30caa715e/src/Data/Empty/Irrelevant.agda>

On Sun, Nov 10, 2019 at 3:47 PM Siek, Jeremy <jsiek at indiana.edu> wrote:

> Is there a form of contradiction that allows irrelevant arguments?
>
> Cheers,
> Jeremy
>
> __________________________________________
> Jeremy G. Siek    <jsiek at indiana.edu>
> Professor
> Luddy School of Informatics, Computing, and Engineering
> Indiana University Bloomington
> http://homes.soic.indiana.edu/jsiek/
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191110/ba07566d/attachment.html>