Inductive Even : nat -> Prop :=
| evenO : Even O
| evenS : forall n, Odd n -> Even (S n) with Odd : nat -> Prop :=
| oddS : forall n, Even n -> Odd (S n). Axiom admit : forall {T}, T. ProgramFixpoint doubleE {n} (e : Even n) : Even (2 * n)
:= admit with doubleO {n} (o : Odd n) : Odd (S (2 * n))
:= _.
Fail Next Obligation of doubleE.
Next Obligation. Admitted.
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
