[Agda] eta expansion

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Mar 8 15:46:58 CET 2013


Is it possible to disable the eta expansion for definitional equality in 
Agda?


More information about the Agda mailing list