| products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (LibreOffice Version 25.8.3.2©) Datei vom 15.8.2025 mit Größe 599 B |
|
Quelle bug_5281.vSprache: Coq |
|||||||||||||||
|
Inductive A (T : Prop) := B (_ : T). Scheme Equality for A. Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}. decide equality. Qed.
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-08-25