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
Afficher les réponses par date