[Agda] eta expansion

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Fri Mar 8 21:02:54 CET 2013


On Fri, Mar 8, 2013 at 2:23 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> Moreover, it would be good to have a pragma MLTT that doesn't allow any
> feature that take us beyond core MLTT (whatever we take that to be).

+1

-- 
Andrés


More information about the Agda mailing list