test-suite/success/cofixtac.v


1
2
3
4
5
6
7
8
9
10

CoInductive stream :=
| C : content -> stream
with content :=
| D : nat -> stream -> content.

Lemma one : stream.
cofix c with (d : content).
- constructor. apply d.
- constructor. exact 1. apply c.
Defined.