Skip to content

[ port idris-lang/Idris2#2863 ] Make some higher-order functions in prelude tc-inlined #34

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mjustus wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[ port idris-lang/Idris2#2863 ] Make some higher-order functions in prelude tc-inlined #34

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions libs/prelude/Prelude/Basics.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
(.:) = (.) . (.)

Expand All @@ -61,20 +61,20 @@ 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

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

Expand Down