Stream: Coq users

Topic: Where `strream` is defined?

view this post on Zulip Daniel Hilst Selli (Jan 19 2022 at 14:43):

I'm trying to follow this tutorial but get The reference stream was not found in the current environment. and have no idea from where to import it. I tried Coq,List.Streams but it not this one, maybe is defined somewhere in CPDT? (this tutorial seems to be a snippet of CPDT)

view this post on Zulip Karl Palmskog (Jan 19 2022 at 14:51):

Custom definition here, it seems:

view this post on Zulip Mycroft92 (Jan 19 2022 at 14:52):

Hi @Daniel Hilst Selli , the definition of stream is given in Coinductives chapter .
You can replace stream with Stream from standard library and the example should go through.

Last updated: Jun 25 2024 at 18:02 UTC