On 2013-04-02 14:45, Serge D. Mechveliani wrote: > 400 lines of Agda have converted to 23413 lines of the Haskell code. Some potential reasons: * Implicit arguments are made explicit. * Things that could be shared (via let, say) aren't. * Terms are normalised. * Things that could be erased aren't. -- /NAD