阅读 Idris2 代码，我已经看到了几个“装饰”函数的案例，%inline而且%tcinline我一直在寻找关于它的清晰解释，但没有找到任何东西，除了它“可以”用于提供一些“提示”以提供帮助对外来电话，但尚不清楚其主要目的是什么以及何时应该使用或何时不应该使用。
此外，如果知道这些恰好开始的“装饰器”是否%有任何共同的目的，那就太好了。
从更改日志：
新函数标志
%tcinline意味着该函数应该内联以进行完整性检查（但否则不内联）。这可以用作完整性检查的提示，使检查器查看原本可能看不到的函数内部。
来自pragmas 的文档：
%inline指示编译器在应用以下定义时内联它。通常最好让编译器和您使用的后端根据其预定规则优化代码，但如果您想在调用函数时强制内联函数，则此编译指示将强制它。