| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/modules/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 611 B |
|
Quelle injection_discriminate_inversion.v Sprache: Coq |
|||||||||||||||
|
Module M. Inductive I : Set := C : nat -> I. End M. Module M1 := M. Goal forall 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. Goal forall 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.
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-09-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10