[Typer] Définitions mutuelles

Bonjour,

J'ai un petit problème avec les définitions mutuelles et je me demandais si quelqu'un avait une idée. Le programme suivant est rejeté.

type Nat | zero | succ (pred : Nat) ;

even : Nat -> Bool; odd : Nat -> Bool;

even n = case n | zero => true | succ p => odd p ;

odd n = case n | zero => false | succ p => even p ;

L'erreur est la suivante.

[X] Fatal :(DEBRUIJN) Unexpected lexp_context shape!

Ça vient de lctx_view qui ne gère que le cas où l'index est 1, et j'imagine que pour de telles définitions récursives, on a 2 par exemple. J'aimerais bien le déboguer moi-même, mais je suis embêté parce que je n'ai aucune idée de ce que fait lctx_view.

Simon