| 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 552 B |
|
Quelle bug_10197.v Sprache: Coq |
|||||||||
|
(* Some check about implicit arguments in fix *)
Check fix f {f:nat} := match f with 0 => true | _ => false end. CoInductive stream := { this : nat ; next : option stream }. Check cofix f {f:nat} := {| this := f ; next := None |}. (* The following was ok from 8.4, just checking that the order is not mixed up accidentally *) Check fix f (x : nat) (x : forall {a:nat}, a = 0 -> nat) := match x eq_refl with 0 => true | _ => false end. Check fix f (x : forall {a:nat}, a = 0 -> bool) (x : nat) := match x with 0 => true | _ => false end. ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28