Stream: Equations devs & users

Topic: Support for Coinductive data

view this post on Zulip Rudy Peterson (Oct 11 2022 at 18:16):

Hello! I am attempting to use coq-equations to write functions over streams but I run into the error

Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.

The code that generated the error was:

CoInductive stream := Stream : nat -> stream -> stream.

Equations stream_map :
  (nat -> nat) -> stream -> stream :=
  stream_map f (Stream n s) :=
    Stream (f n) (stream_map f s).

Does equations support coinductive elimination?

Thanks!

view this post on Zulip Paolo Giarrusso (Oct 11 2022 at 19:07):

maybe not yet — based on https://github.com/mattam82/Coq-Equations/issues/490 and on https://github.com/mattam82/Coq-Equations/search?q=coinductive finding nothing

Last updated: Apr 19 2024 at 13:02 UTC