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!
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: Nov 29 2023 at 18:01 UTC