Inductive even: nat -> Prop :=
| evenB: even 0
| evenS: forall n, even n -> even (S (S n)).
Goal even 1 -> False. Proof.
refine (fun a => match a withend). Qed.
Goal even 1 -> False. Proof.
refine (fun a => match a in even n returnmatch n with 1 => False | _ => True end : Prop with evenB => I | evenS _ _ => I end). Qed.
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.
