在Idris上真正做的是什么？什么时候使用它？

Question

阅读Idris2代码时，我看到了几个用%inline和%tcinline“修饰”函数的例子，我一直在寻找关于它的明确解释，但是除了“可以”用来给出一些“提示”来帮助外接电话之外，我还没有找到任何东西，但不清楚它的主要用途是什么，什么时候应该使用，什么时候不应该使用。

另外，如果知道这些从%开始的“装潢师”是否有任何共同的目的，那就太好了。

Answer 1

来自变更日志

新函数标志%tcinline，这意味着函数应该内联，以便进行总体检查(但否则不能内联)。这可以用作总体检查的提示，以使检查器查看函数内部，否则它可能不会。

来自关于语用的文件

%inline指示编译器在应用时内联如下定义。通常最好让编译器和您正在使用的后端基于其预定的规则来优化代码，但是如果您想在调用函数时强制将其内联，则此实用程序将强制它。