[Agda] making a pair explodes

Jacques Carette carette at mcmaster.ca
Mon Apr 17 16:24:58 CEST 2017


 >  What is the type of _,_ exactly?

Full dependent product.  Sometimes _,'_ can be considerably faster if cartesian product is what is wanted.

Jacques




More information about the Agda mailing list