20 Fév
2017
20 Fév
'17
17:02
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