[isabelle] Module dependence cycle when generating code using gfp for SML and OCaml



Hi,

Consider the following silly definition (in Isabelle2016-1):

definition goo :: "bool set" where
  "goo â gfp (Îx. x â {})"

And the following code generation commands:

export_code goo in Scala
export_code goo in Haskell

export_code goo in SML
export_code goo in OCaml

The first two commands for the Scala and Haskell targets succeed, and
generate code, but the second two do not and instead produce the
following error:

Dependency "ccpo" < "Sup" -> class "Sup" would result in module dependency cycle

The problem appears to be the gfp and lfp constants.  How can I work
around this and generate SML code using gfp (and lfp)?

Thanks,
Dominic




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.