[Agda] evaluation strategies of the future [issue #426]

Ulf Norell ulf.norell at gmail.com
Fri Oct 28 13:29:46 CEST 2016


On Fri, Oct 28, 2016 at 11:57 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> Can anybody provide a small and clear example having an exponential type
> check cost both with --sharing and without it?
>

I assume you also mean ".. but which one would expect not to be exponential
under call-by-need".

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161028/e898c981/attachment.html


More information about the Agda mailing list