Quelle injection_discriminate_inversion.v
Sprache: Coq
Module M. Inductive I : Set := C : nat -> I. End M.
Module M1 := M.
Goalforall x, M.C x = M1.C 0 -> x = 0 . intros x H. (* injection sur deux constructeurs egaux mais appeles par des modules differents
*) injection H. tauto. Qed.
Goal M.C 0 <> M1.C 1. (* Discriminate sur deux constructeurs egaux mais appeles par des modules differents
*) intro H;discriminate H. Qed.
Goalforall x, M.C x = M1.C 0 -> x = 0. intros x H. (* inversion sur deux constructeurs egaux mais appeles par des modules differents
*) inversion H. reflexivity. Qed.
Messung V0.5
¤ Dauer der Verarbeitung: 0.12 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 und die Messung sind noch experimentell.
