| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 367 B |
|
Quelle bug_4588.vSprache: Coq |
|||||||||||||||
|
Set Primitive Projections. (* This proof was accepted in Coq 8.5 because the subterm specs were not projected correctly *) Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }. Fail Fixpoint loop (x : foo) : False := loop (proj2 x _ x). Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-27