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<mailto: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<mailto: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
