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

Sergei Meshveliani mechvel at botik.ru
Fri Oct 28 14:40:23 CEST 2016


On Fri, 2016-10-28 at 13:29 +0200, Ulf Norell wrote:
> 
> 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".


Уеs, thank you.






More information about the Agda mailing list