[Agda] irrelevant fields and EqReasoning

[Nils Anders Danielsson]

On 2012-07-20 21:40, Noam Zeilberger wrote:
> For anyone interested, here is an alternate implementation of
> PreorderReasoning that pushes the types through explicitly, rather
> than relying on constraint solving (which as Andreas explained will
> fail when there are irrelevant fields).  This gets rid of the unsolved
> metas in my original example.

Have you checked how this change affects the performance of
type-checking?

-- 
/NAD