blob: 296e4e11e5f294b78f930f2eec8591eb79d6a1d5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Fix and Cofix were missing in tactic unification *)
Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
= (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
Proof.
eexists.
reflexivity.
Qed.
CoInductive stream := cons : nat -> stream -> stream.
Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
Proof.
eexists.
reflexivity.
Qed.
|
