[Agda] performance debugging?

[mechvel at scico.botik.ru]

On 2023-09-26 17:37, Nils Anders Danielsson wrote:
> On 2023-09-25 16:21, Robby Findler wrote:
>> 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?
> 
> I assume that you refer to the new keyword "opaque".
> 
> Definitions which unfold "too much" can make Agda slow. If you have
> definitions which usually do not need to be unfolded, then you can mark
> them as opaque. If there is a need to unfold such a definition in a
> proof (say), then you can make the definition transparent in the proof,
> if you also make the proof opaque.


Suppose one writes

   lemma1 :  (n : Nat) -> f n ≡ g n
   lemma1 =  <lengthy implementation for the proof>

and  lemma1  is used several times
as  (lemma 1), (lemma 2), (lemma 3) ...

without analyzing the structure of the proof of (lemma i).
Will it make the type check faster setting  lemma1  under `opaque' ?

Regards,

------
Sergei