[Agda] Identifying inefficiency
Wolfram Kahl
kahl at cas.mcmaster.ca
Tue Mar 26 17:42:45 CET 2019
On Tue, Mar 26, 2019 at 03:33:11PM +0000, Martin Escardo wrote:
> (I tried supplying all the implicit arguments to the RHS's, but the 30s
> time remains the same. At the holes, the types of the subterms of the
> terms that I want to fill the holes with is known, so I am not sure what
> is going on. But I guess this is a different question from the one in
> this thread.)
Perhaps you are in the kind of situation that I frequently encounter,
see https://github.com/agda/agda/issues/1625 .
I haven't tried Andrea's patch at
https://github.com/agda/agda/issues/1625#issuecomment-132196576
in a while, but it worked wonders for some developments that would
otherwise have been impossible to typecheck.
Wolfram
More information about the Agda
mailing list