阅读 Idris2 代码，我已经看到了几个“装饰”函数的案例，%inline而且%tcinline我一直在寻找关于它的清晰解释，但没有找到任何东西，除了它“可以”用于提供一些“提示”以提供帮助对外来电话，但尚不清楚其主要目的是什么以及何时应该使用或何时不应该使用。
此外，如果知道这些恰好开始的“装饰器”是否%有任何共同的目的，那就太好了。
在 Haskell 中the，我无法将几种类型定义放在一起来理解它们，这些定义是否有共同的目的？如果是这样是什么？即来自 Hoggle 的一些：
the :: Eq a => [a] -> a
the :: HasAny sel s t a b => Lens s t a b
the :: (Eq a, Monad m) => SerialT m a -> m (Maybe a)
等等。