I was trying to make an (infinite) `Stream`

that goes something like

```
[0,1,2,3,4,5,....]
```

I tried to do this with

```
Require Import Streams.
CoFixpoint incStream (s:Stream nat):Stream nat :=
match s with
| Cons x xs => Cons (x+1) xs
end.
CoFixpoint foo:Stream nat := Cons 1 (incStream foo).
```

But that didn't work.

```
Recursive definition of foo is ill-formed.
In environment
foo : Stream nat
Unguarded recursive call in
"cofix incStream (s : Stream nat) : Stream nat :=
match s with
| Cons x xs => Cons (x + 1) xs
end".
Recursive definition is: "Cons 1 (incStream foo)".
```

Any idea how this can be done?

```
CoFixpoint incStream (n:nat):Stream nat := Cons n (incStream (S n)).
Definition foo := incStream 1.
```

Thanks! It works.

Julin S has marked this topic as resolved.

Last updated: Oct 03 2023 at 21:01 UTC