One post tagged with "mutual"

In this blog post, we present a technique with the  Rocq/Coq theorem prover to define mutually recursive functions using a notation. This is sometimes convenient for types defined using a container type, such as types depending on a list of itself.