From e0f78b490425b502c1e799bd2fb3e06bf0b8230d Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Wed, 25 Oct 2023 16:32:07 +0100 Subject: [PATCH] [ port idris-lang/Idris2#2863 ] Make some higher-order functions in prelude tc-inlined Co-authored-by: Denis Buzdalov --- libs/prelude/Prelude/Basics.idr | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr index 2a1baf23..c5300c28 100644 --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -37,14 +37,14 @@ const : a -> b -> a const x = \value => x ||| Function composition. -public export %inline +public export %inline %tcinline (.) : (b -> c) -> (a -> b) -> a -> c (.) f g = \x => f (g x) ||| Composition of a two-argument function with a single-argument one. ||| `(.:)` is like `(.)` but the second argument and the result are two-argument functions. ||| This operator is also known as "blackbird operator". -public export %inline +public export %inline %tcinline (.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d (.:) = (.) . (.) @@ -61,7 +61,7 @@ public export %inline ||| ```idris example ||| sortBy (compare `on` fst). ||| ``` -public export +public export %tcinline on : (b -> b -> c) -> (a -> b) -> a -> a -> c on f g = \x, y => g x `f` g y @@ -69,12 +69,12 @@ infixl 0 `on` ||| Takes in the first two arguments in reverse order. ||| @ f the function to flip -public export +public export %tcinline flip : (f : a -> b -> c) -> b -> a -> c flip f x y = f y x ||| Function application. -public export +public export %tcinline apply : (a -> b) -> a -> b apply f a = f a