问编译器:没有为排序Optional[KVar]定义新生成器
EN

Stack Overflow用户

提问于 2020-03-26 01:38:06

回答 1查看 25关注 0票数 0

我正在使用LLVM后端进行编译。它可以使用Java后端进行编译，但是LLVM后端会引发以下错误：Compiler: No fresh generator defined for sort Optional[KVar]

该错误突出显示了!M中的<abs> ... .Map => (!M |-> (T1 -> T2)) ... </abs>。

回答已采纳

发布于 2020-03-26 11:00:59

这是K的替换实现中的一个错误，它导致KVar排序的新常量只能在java后端上可用。您可以在这里跟踪问题：https://github.com/kframework/k/issues/1186

我们很快就会设法解决这个问题，因为它应该是直截了当的。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/60859837

复制

相似问题

问编译器:没有为排序Optional[KVar]定义新生成器EN