[Agda] evaluation in compilation

Nils Anders Danielsson nad at chalmers.se
Wed Oct 3 07:44:39 CEST 2012


On 2012-10-02 22:22, Serge D. Mechveliani wrote:
> For example, an algorithm of the cost  O(n^2)  needs to be programmed
> in Agda also as taking  O(n^2),  not O(n^3).

Are you saying that you're implementing a quadratic algorithm, but that
Agda somehow makes it cubic? Can you give an example?

-- 
/NAD


More information about the Agda mailing list