Stream: Coq users

Topic: ✔ Infinite list


view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Sep 05 2022 at 09:10):

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

view this post on Zulip Julin S (Sep 05 2022 at 09:14):

Thanks! It works.

view this post on Zulip 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