[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