如何解决%inline 在 Idris 上到底做了什么?什么时候使用它?
阅读 Idris2 代码我见过几个用 %inline
和 %tcinline
“装饰”的函数我一直在寻找关于它的明确解释,但除了它之外没有找到任何东西“可以”用于给出一些“提示”,以帮助外来电话,但不清楚它的主要用途是什么,什么时候应该使用,什么时候不应该使用。
此外,如果知道这些碰巧以 %
开头的“装饰器”是否有任何共同目的,那就太好了。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。