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)) (evenS (); mais je ne comprends ce que `forall x:nat, even x -> even (S (S x))` fait en temps que tel. -- Pierre Delaunay
Afficher les réponses par date
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
participants (2)
-
Pierre Delaunay -
Stefan Monnier