| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 567 B |
|
Quelle bug_3125.v Sprache: Coq |
|||||||||
|
(* Not considering singleton template-polymorphic inductive types as
propositions for injection/inversion *) (* This is also #4560 and #6273 *) #[universes(template)] #[warnings="-no-template-universe"] Inductive foo := foo_1. Add Keep Equalities foo. Goal forall (a b : foo), Some a = Some b -> a = b. Proof. intros a b H. inversion H. reflexivity. Qed. (* Check that Prop is not concerned *) Inductive bar : Prop := bar_1. Goal forall (a b : bar), Some a = Some b -> a = b. Proof. intros a b H. inversion H. Fail reflexivity. Abort. ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28