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 +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
