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