Julin S (Sep 05 2022 at 09:07): Julin S (Sep 05 2022 at 09:07):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?
Guillaume Melquiond (Sep 05 2022 at 09:10):CoFixpoint incStream (n:nat):Stream nat := Cons n (incStream (S n)).
Definition foo := incStream 1.
Thanks! It works.
Notification Bot (Sep 05 2022 at 09:19):Julin S has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC