<div dir="ltr">Hi all-- I'm having some performance trouble with an agda development I'm working on. I made a change to some low-level data structure and am now working my way through the rest of the code doing the required updates. Some of the updates require me to add a new argument alongside an existing one and as I'm working through the cases in a lemma, doing that, I'm at the point in a 200 line file where it takes about 12 minutes for agda to check it. There seemed to be a large jump after I repaired one of the cases (from a bit less than a minute to about 5 minutes; this was when I was in the stage of getting errors instead of having holes to fill in).<br><br><div>Anyway, all that is context to ask if there is any advice on things I might do to try to get back to more interactive speeds. I tried filling (nearly) all of the implicit parameters in the case that had the large jump, but that didn't seem to help (although filling in implicit arguments explicitly has seemed to help in other situations). Are there other things one might try? </div><div><br></div><div>I'm still on 2.6.3, if that matters. I see that there is a performance related change in 2.6.4: is there a way to get some hints about which functions might benefit from that treatment?<br></div><br>Thanks in advance!<br><br>Best,<br>Robby</div>