edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-28 07:15:33 +03:00
Code Issues Projects Releases Wiki Activity

Add curry/uncurry to Prelude

Browse Source
This commit is contained in:
Edwin Brady 2019-10-13 12:12:49 +01:00
parent 519415f82f
commit a162425384
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/prelude/Prelude.idr
View File

@ -86,6 +86,14 @@ public export
apply : (a -> b) -> a -> b apply : (a -> b) -> a -> b
apply f a = f a apply f a = f a
public export
curry : ((a, b) -> c) -> a -> b -> c
curry f a b = f (a, b)
public export
uncurry : (a -> b -> c) -> (a, b) -> c
uncurry f (a, b) = f a b
-- $ is compiled specially to shortcut any tricky unification issues, but if -- $ is compiled specially to shortcut any tricky unification issues, but if
-- it did have a type this is what it would be, and it might be useful to -- it did have a type this is what it would be, and it might be useful to
-- use directly sometimes (e.g. in higher order functions) -- use directly sometimes (e.g. in higher order functions)