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.
🦄 Mutually recursive functions with notation
· 4 min read