While we have some examples of mutually recursive functions in the gallery
(e.g., http://toccata.lri.fr/gallery/defunctionalization.en.html), I was
only able to find a single instance of a mutually-recursive type
definition. It is in the Pairing Heaps development, module HeapType:
Hi,
You can define mutually recursive types using “with” (instead of the more
common “and”). For example,
type tree ‘a = Empty | Node ‘a (forest ‘a)
with forest ‘a = Nil | Cons (tree ‘a) (forest ‘a)
I was in a similar situation a few weeks ago and couldn’t find any
documentation then.
Is there a way to define mutually recursive types in WhyML? I couldn't find
one in the documentation. If not, is there a standard recommended
workaround?
For context, in our course I am doing a little exploration and Dynamic
Logic,
and in Dynamic Logic formulas and programs are defined in a
