Re: [Typer] Recursion et Indices de Debruijn

    tonum = lambda x -> case x           %
        | (succ y) => (1 + (tonum y))    %  ENV: [tonum[2]; x[1]; y[0]]
        | _ => 0;

tonum marche pour seulement une récursion parce que pour le second appel à tonum l'index de tonum n'est plus 2 mais 4 (2 x et 2 y).

Non. Lors de l'appel récursif, tu reprends l'environnement de tonum (i.e. où il n'y avait pas encore de x ni de y) et tu y ajoutes un nouveau x et ensuite un nouveau y.

Ça fait partie de la différence entre lexical-scoping et dynamic-scoping.

Stefan