[Agda] Should we create an issue to track the status of Cubical?

Apostolis Xekoukoulotakis apostolis.xekoukoulotakis at gmail.com
Mon Sep 18 07:49:27 CEST 2017


I have recently learned to program with CTT. I was trying to understand the
consequences
it will have in programming. For now, I will just go back to my usual
programming
but I would like to be notified when quotient types or Higher Inductive
types are ready
so as to start using them as soon as possible.

For this reason, I propose that we create an issue to track the development
of these features.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170918/559ee5fd/attachment.html>


More information about the Agda mailing list