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?
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: May 28 2023 at 18:29 UTC