[Agda] pattern matching on records

[Amr Sabry]

How does one do "deep" pattern matches on records involving dot
patterns. Is it even possible? In the attached program 'simplify' should
have the "obvious" definition commented at the bottom but nothing I can
write will allow Agda to infer or even pattern match on the implicit
arguments. Any help would be appreciated. Thanks. --Amr

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Q.agda
Type: application/octet-stream
Size: 1000 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140630/b93059ea/Q.obj