Hi Florian, One more thing: The indirect recursion causes SML/OCaml code generation to fail, but converting to the equivalent mutual-recursive definition makes it work again.
datatype 'a tree = Node 'a "'a tree list" definition "test2 = (Node True [] = Node True [Node False []])" export_code test2 in OCaml file - *** Illegal mutual dependencies: "tree :: eq", "eq_class.eq [tree]" *** At command "export_code". datatype 'a tree = Node 'a "'a forest" and 'a forest = Empty | Trees "'a tree" "'a forest" definition "test2 = (Node True Empty = Node True (Trees (Node False Empty) Empty))" export_code test2 in OCaml file - The second version works just fine for OCaml or SML. I would have expected both versions of the tree datatype to produce basically the same code for eq, since they both have essentially the same recursion combinator. - Brian
