[Agda] Agda equalType variation

[Ulf Norell]

On Tue, Mar 10, 2009 at 5:52 PM, Remi Turk <rturk at science.uva.nl> wrote:

>
> So my question is, is there a variation of equalType that _is_ able
> to see through abstract types?
>

ignoreAbstractMode (equalType a b)

ignoreAbstractMode is exported by Agda.TypeChecking.Monad

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090310/eee97644/attachment.html