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

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?


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

maybe not yet — based on and on finding nothing

Last updated: Nov 29 2023 at 18:01 UTC