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)
Custom definition here, it seems: http://adam.chlipala.net/cpdt/html/Coinductive.html#stream
Hi @Daniel Hilst Selli , the definition of
stream is given in Coinductives chapter .
You can replace
Stream from standard library and the example should go through.
Last updated: Feb 01 2023 at 12:30 UTC