[Agda] Re: Irrelevant record fields

Andrea Vezzosi sanzhiyan at gmail.com
Sat Sep 25 00:51:37 CEST 2010


Hi Andreas,
I've replied to the other message before seeing this one, which
contains exactly what i was looking for, thanks!
Now i'll see what happens when one tries to apply the approach to a CT library.


More information about the Agda mailing list