<div dir="ltr"><div>Hi all-- This morning I was working on a lemma that really seems like it is taking longer than it should. I tried all the approaches that various folks sent me in this thread
 (lossy-unification, no-infer-absurd-clauses, opaque declarations -- thank you!) but, alas, was not able to get any improvements. (I'm not sure 
that I made the right definitions opaque, tho!). </div><div><br></div><div>The lemma takes in two related arguments and, instead of being O(n^2) cases in the constructors, it is O(n) because of the relationship. Each time I load this lemma, it takes 7.5 minutes (using "time agda file.agda" on a file containing only this lemma whose imports are all already checked). After the initial case split, it was taking maybe 2-3 minutes to load the file (with each rhs just being a hole), in case that seems important. A different lemma that I was working on yesterday takes similar arguments except there is only one (not two) of these one arguments and I can work on that one at basically interactive speeds (just some seconds to load that lemma). According to the Emacs mode, the thing that takes most of the time is when the entire function is highlighted (not the individual cases, although those aren't speedy either).<br></div><div><br></div><div>Assuming this description doesn't spark any ideas that others might have that I could try, I was wondering if anyone more versed in agda performance might be willing to have a look? I've trimmed down the development to just the file that has the overly slow lemma and its dependencies (it also depends on the iowa agda library, not the standard lib that comes with agda which I've not yet learned...). It is still pretty big, I'm sorry to say, at nearly 1800 lines (not counting what it uses in ial), but the file with the bad lemma is 118 lines. I don't think I'm doing anything particularly sophisticated in this code. (I'm no agda guru! :).<br></div><div><br></div><div>tia, Robby<br></div><div><br></div><div><br></div></div>