Je ne comprends pas comment définir en Typer: Inductive even: nat -> Prop := % Premier axiome | even0 : even 0 % Deuxième axiome | evenS : forall x:nat, even x -> even (S (S x)).

j'ai quelque chose comme:

even : Type; even = typecons (even (n : Nat)) (even0 (Eq (t := Nat) zero n))

C'est juste.

(evenS (); mais je ne comprends ce que `forall x:nat, even x -> even (S (S x))` fait en temps que tel.

Dans Typer, `forall x:t1, t2` s'écrit `(x : t1) -> t2`. Donc ça fait qqch du genre:

(evenS (x : Nat) (Even x) (Eq (t := Nat) (S (S x)) n)

[ Remarque que j'utilise par convention des identificateurs capitalized pour les types. ]

Donc tu as ici d'une part l'usage du `Eq` et d'autre part l'usage de typage dépendant (ou le type du deuxième champ (Even x) dépend de la *valeur* du premier).

Stefan