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
Afficher les réponses par date
participants (1)
-
Génier Simon