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

Andrea Vezzosi sanzhiyan at gmail.com
Mon Sep 18 10:06:01 CEST 2017


Here it is, and thanks for checking cubical out!

https://github.com/agda/agda/issues/2761

Cheers,
Andrea

On Mon, Sep 18, 2017 at 7:49 AM, Apostolis Xekoukoulotakis
<apostolis.xekoukoulotakis at gmail.com> wrote:
> 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


More information about the Agda mailing list