Je pensais plus à quelque chose comme cela:
Nat = inductive_ (dNat) (zero) (succ Nat);
zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;
one = (succ zero); two = (succ one); three = (succ three);
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). La solution que j'avais pensé était de push le body de tonum à l'appel de la fonction ainsi la distance du body de tonum est toujours de 2. (Cela revient à traiter tonum comme une fonction avec un argument implicite qui est lui même) Sinon il faut calculer pendant l'évaluation l'offset de tonum ce qui serait certainement plus efficace.