blob: 6aeb05f54ec5e3277ee35e624bbf325001a302b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* cbn is able to refold mutual recursive calls *)
Fixpoint foo (n : nat) :=
match n with
| 0 => true
| S n => g n
end
with g (n : nat) : bool :=
match n with
| 0 => true
| S n => foo n
end.
Goal forall n, foo (S n) = g n.
intros. cbn.
match goal with
|- g _ = g _ => reflexivity
end.
Qed.
|
