在導出代碼中爲Scala修復醜陋的字符串導出

我有一個功能foo，它可以在string類型上工作。當我export_code foo in Scala file -我得到一個非常醜陋的Scala代碼。在導出代碼中爲Scala修復醜陋的字符串導出

一個很長的列表，看起來像這樣創建

abstract sealed class nibble 
final case class Nibble0() extends nibble 
final case class Nibble1() extends nibble 
final case class Nibble2() extends nibble 
...

來源

2013-03-07 corny

伊莎貝爾/ HOL？！？哇。 – 2013-03-07 16:13:19

Isabelle擁有多種語言的代碼生成功能，包括Scala和Haskell – 2013-03-07 21:32:41

你需要導入Code_Char理論，以告訴代碼生成使用字符/字符串的現有實現在目標語言，而不是將Isabelle定義翻譯爲數據類型。

將"~~/src/HOL/Library/Code_Char"添加到您的理論的導入條款，一切都應該正常工作。

此外，我被告知 - 但無法驗證這一點 - 這應該總是在您的導入子句的末尾，因爲否則，有趣的事情發生在代碼生成器。

乾杯，曼努埃爾·斯卡拉

來源

2013-03-07 12:31:01

在導出代碼中爲Scala修復醜陋的字符串導出

回答

相關問題