Re: [isabelle] Scala generator



Am 01.02.2011 14:46, schrieb René Thiemann:
we have not yet simplified and localized the exact problem
The problem seems to be that the code generator doesn't generate the necessary "val ... = " parts for values that are not used anywhere and the resulting anonymous function isn't a valid statement on it's own.

A simpler example might be:

theory Test
imports Main
begin

definition myfun :: "bool"
where "myfun \<equiv> let x =  \<lambda> l::bool. True
  in True"

export_code myfun in Scala file "Test.scala"
end

which produces:

object Test {

def myfun: Boolean = {
                       (_: Boolean) => true;
                       true
                     }

} /* object Test */





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