是否可以将 Lean 语言(从 Lean 4)导出到其他语言，就像 Isabelle 通过代码生成导出到 Haskell 或 Scala 一样？
在文档中没有找到它。
最佳答案
不，这样做通常是一个坏主意。 Lean 的运行时性能，特别是对于Array 等基本类型，从根本上依赖于 "functional but in-place" technique 。使用跟踪垃圾收集器实现的语言通常无法实现这种运行时优化，因此在例如以下情况时必须回退到保守复制:修改数组。
更好的方法是认识到精益本身就是一种通用语言，并使用它的 foreign-function interface (是的，在撰写本文时尚未完全完成和稳定，但已被一些人成功使用)与其他语言编写的代码进行交互。
关于code-generation - Lean 4 将代码导出为其他语言，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/74301506/