This is similar to the earlier post Blazingly Fast™ Type Class Resolution with Tries. Both use tries for instance resolution, but Agda has more implementation details due to more flexibility in its instances (and actually has an implementation).
You must log in or register to comment.