| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 407 B |
|
Quelle bug_17093.vSprache: Coq |
|||||||||||||||
|
Inductive sTrue : SProp := sI. (* Singleton Prop to SProp *) Definition elim0 (x : False) : sTrue := match x return sTrue with end. Definition elim0' (x : False) : sTrue := match x with end. (* Non-singleton Prop to SProp *) Definition elim1 (x : inhabited nat) : sTrue := match x return sTrue with inhabits _ => sI end. Definition elim1' (x : inhabited nat) : sTrue := match x with inhabits _ => sI end.
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-27