[Agda] irrelevant contradiction?

[Siek, Jeremy]

Thanks!

On Nov 10, 2019, at 10:52 AM, Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis at gmail.com<mailto:apostolis.xekoukoulotakis at gmail.com>> wrote:

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<mailto:jsiek at indiana.edu>> wrote:
Is there a form of contradiction that allows irrelevant arguments?

Cheers,
Jeremy

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto: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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Professor
Luddy School of Informatics, Computing, and Engineering
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191111/0193522a/attachment.html>