aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity/f_equal.v
blob: 86698fa87289086dcbe9b157c1a81d5ea97c1897 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(* 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.