| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/complexity/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 357 B |
|
Quelle Notations.v Sprache: Coq |
|||||||||
|
(* Last line should not loop, even in the presence of eta-expansion in the *)
(* printing mechanism *) (* Expected time < 1.00s *) Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at level 0, y at level 0,format "'[hv' 'bind' x <- y ; '/' z ']'"). Definition f (g : (nat -> nat) -> nat) := g (fun x => 0). Time Check (fun g => f g). ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28