+Nat_add n k = case n

• | (succ n) => Nat_add n (succ k)
• | zero => k;

Habituellement, on utilse la forme avec une récursion non-terminale:

Nat_add n k = case n | succ n => succ (Nat_add n k) | zero => k;

pas sûr exactement pourquoi (quoique: voir ci-dessous `len`).

+Nat_eq : Nat -> Nat -> Type; +Nat_eq n k = case (n,k)

• | (succ n,succ k) => Nat_eq n k
• | (zero,zero) => True
• | False;

Je suis content de voir que tu es confortable à construire des types dans une fonction. Mais je crois que cette fonction n'est pas nécessaire.

+type List_n (n : Nat) (a : Type)

• | cons a (List_n sn a) (p ::: (Nat_eq n (succ sn)))
• | nil (p ::: (Nat_eq n zero));

Tu utilises `sn` sans le définir. Plus précisément, tu dois faire:

type List_n (n : Nat) (a : Type) | cons (sn ::: Nat) a (List_n sn a) (p ::: (Nat_eq n (succ sn))) | nil (p ::: (Nat_eq n zero));

Idéalement, tu devrais pouvoir écrire ça comme ça:

type List_n (n : Nat) (a : Type) | cons a (List_n ?sn a) (p ::: (Nat_eq n (succ ?sn))) | nil (p ::: (Nat_eq n zero));

mais j'ai l'impression que c'est pas encore implanté.

Par contre, une autre simplification est que tu devrais pouvoir utiliser `Eq` au lieu de `Nat_eq`.

+len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat; +len xs = case (xs)

• | cons x xs => succ (len xs)
• | nil => zero;

Si tu veux montrer que

∀ l : List_n n α . Eq n (len l)

je pense que la définition de `len` que tu utilises fonctionnera mieux avec l'autre définition de Nat_add (à l'inverse, ta définition de Nat_add fonctionnera mieux avec une définition tail-recursive de `len`).

+%prep : (n : Nat) ≡> a -> List_n n a -> List_n (succ n) a; +%prep x xs = cons (n := (succ n)) x xs (Nat_eq (succ n) (succ n));

^^^^^^^^^^^^^^^^^^^^^^^^^^ devient Eq_refl

-- Stefan