Re: [Why3-club] [Why3] Mutually recursive types?

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.

[Why3-club] (no subject)

attempted using Coq. Are there plans to add an instance in a future release? If not, how might I go about modifying my existing Why3 installation to include one? Thanks, Ramana Nagasamudram ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https