[Agda-dev] Design question about eta-equality for records

[Andreas Abel]

Hello developers,

I made a proposal how Agda should handle eta for records in a safe way:

   https://github.com/agda/agda/issues/2436#issuecomment-275760272

Please approve :) (or discuss).

--Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/