Re: [isabelle] Problem with Scala code generation



>> 1) There are too few brackets: 
>> definition problem 
>>  where "problem b opt \<equiv> b \<or> (case opt of
>>                 None \<Rightarrow> True | Some _ \<Rightarrow> False)"
>> 
>> export_code problem in Scala module_name Problem file "Problem.scala"
>> 
>> yields 
>> 
>> object Problem {
>> 
>> def problem[A](b: Boolean, opt: Option[A]): Boolean =
>>  b || opt match {
>>         case None => true
>>         case Some(_) => false
>>       }
>> 
>> } /* object Problem */
> 
> congratulations, you have found a bug!  To circumvent it, wait for the
> next Isabelle release or help yourself with something like
> 
> code_const HOL.conj and HOL.disj
>  (Scala "!(_ && _)" and "!(_ || _)")

Thanks,
René




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