[Agda] test report

[mechvel at scico.botik.ru]

On 2021-03-30 20:55, Nils Anders Danielsson wrote:
> On 2021-03-30 01:04, mechvel at scico.botik.ru wrote:
>> The run-time performance remains (it was satisfactory)
>> - must it remain?
> 
> No, but if your program was fairly optimised I am not surprised that 
> the
> execution time did not change a lot. Even without the @0 annotation 
> Agda
> erases certain things, and due to lazy evaluation things that are not
> erased might not be evaluated.
> 
> However, one can construct programs where the annotation makes a
> difference.
> [..]

I see, thank you.

--
SM