| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 304 B |
|
Quelle bug_3310.vSprache: Coq |
|||||||||||||||
|
Set Primitive Projections. Set Implicit Arguments. CoInductive stream A := cons { hd : A; tl : stream A }. CoFixpoint id {A} (s : stream A) := cons (hd s) (id (tl s)). Lemma id_spec : forall A (s : stream A), id s = s. Proof. intros A s. Fail change (id s) with (cons (hd (id s)) (tl (id s))). Abort.
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09