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: http://toccata.lri.fr/gallery/pairing_heap.en.html
In this example, one can also find a certain number of mutually recursive functions and lemma functions. On the standard library, there is the definition of n-ary trees: http://why3.lri.fr/stdlib/tree.html Best regards -- Mário Pereira Ramana Nagasamudram <rnaga...@stevens.edu> escreveu no dia segunda, 1/03/2021 à(s) 22:30: > 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. > > > Best, > Ramana > > On Mar 1, 2021, at 4:40 PM, Frank Pfenning <f...@cs.cmu.edu> wrote: > > 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 mutually > recursive way. > > Programs alpha, beta ::= x <- e | (alpha ; beta) | alpha u beta | alpha* | > ?P > Formulas P, Q := e1 <= e2 | ... | P /\ Q | ... | [alpha]P | <alpha>P > > I'd like to avoid defining tests ?P separately from formulas. > > Thanks, > Frank > > -- > Frank Pfenning, Professor > Computer Science Department > Carnegie Mellon University > Pittsburgh, PA 15213-3891 > > http://www.cs.cmu.edu/~fp > <https://nam02.safelinks.protection.outlook.com/?url=http:%2F%2Fwww.cs.cmu.edu%2F~fp&data=04%7C01%7Crnagasam%40stevens.edu%7Cb9b9dc059b794a09de6808d8dcfaa830%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C1%7C637502316434530051%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=x41Vc9ZS5iEq1Ju1gIWk254YL6LOw%2B9lRzUf07v9VX0%3D&reserved=0> > +1 412 268-6343 > GHC 6017 > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
