[Agda] Size limit on generated code?

[Roly Perera]

Yes, and there's also the opportunity to erase unused indices (and
indeed not doing so can compromise asymptotic complexity, as discussed
here: https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis).

Maybe this happens already, though.

On 29 September 2014 04:04, Peter Hancock <hancock at fastmail.fm> wrote:
> A lot of the "proofs" might not be run-time-relevant