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