(* Checks that f_equal does not reduce the term uselessly *)
(* Expected time < 1.00s *)
Fixpoint stupid (n : nat) : unit :=
match n with
| 0 => tt
| S n =>
let () := stupid n in
let () := stupid n in
tt
end.
Goal stupid 23 = stupid 23.
Timeout 5 Time f_equal.
Abort.
| Messung V0.5 in Prozent |
|---|
| | | |
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet am 2026-06-04)
¤
*© Formatika GbR, Deutschland
