[Agda] performance debugging?

[Nils Anders Danielsson]

On 2024-04-25 20:06, Robby Findler wrote:
> 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.

> 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).

Your code may only contain "O(n)" cases, but I suspect that Agda still
does some work to discard the remaining cases. I've recently optimised
code with similar characteristics. Perhaps you can do something similar:

* Prove suitable inversion lemmas for one of the two types.

* Instead of matching on both arguments, match on one, and use inversion
  lemmas for the other argument.

-- 
/NAD