blob: c98689c234058d69832e3b264589273331ebd4f2 (
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.
|
