[Agda] result code explosion

Nils Anders Danielsson nad at chalmers.se
Thu Apr 4 15:35:39 CEST 2013


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


More information about the Agda mailing list