[Agda] eta expansion

Martin Escardo m.escardo at cs.bham.ac.uk
Mon Mar 11 12:00:04 CET 2013



On 09/03/13 09:03, Andreas Abel wrote:
>   One the way, one would probably identify the fragment of Agda which is
> justifiable in MLTT.

Yes, this is what I think would be useful.

Also, simply "justifiable" (omitting MLTT) would be good too.

Best,
Martin



More information about the Agda mailing list