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)

http://adam.chlipala.net/cpdt/html/GeneralRec.html

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

Custom definition here, it seems: http://adam.chlipala.net/cpdt/html/Coinductive.html#stream

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: Sep 23 2023 at 07:01 UTC