[isabelle] Code-Export: SML value restriction problem?



Hi, I ran into the following problem, where a code generation to SML
produces invalid SML code:

theory Scratch
imports MainÂ
begin
ÂÂ
definition "foo â Some (Some o fst)"
Â
export_code foo checking SMLÂ
 (*** ROOT.ML:7: error: Type ('a * 'b -> 'a option) option includes a
free type variable *)

When, however, unfolding the function composition, everything works
fine:

definition "bar â Some (Îx. Some (fst x))"
export_code bar checking SML
 (* No error *)

What happened here? Is this a bug in the code generator, or a known
limitation?Â
--
 Peter

p.s. The generated Scala code is valid in both cases.





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