Re: [isabelle] Isabelle2015-RC0 available for testing



>   export_code "gcd::intâintâint" in SML
> 
> fails in Isabelle2015-RC0, with message:
> 
>   Dependency "int" :: "semiring_div_parity" -> "int" ::
> "semiring_parity" would result in module dependency cycle

I encountered a similar problem a while ago:


<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/9323>

Sometimes, these kinds of cycles cannot be avoided in the code generator
setup. The workaround is trivial, though:

  export_code "gcd::intâintâint"
    in SML module_name GCD

Cheers
Lars




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