idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ base ] Make foldr1 and foldr1By public

Browse Source
This commit is contained in:
Steve Dunham 2023-08-06 15:04:06 -07:00 committed by G. Allais
parent 3ce8b9f9cb
commit badf1e98c8
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG.md
View File

@ -183,6 +183,8 @@
* Adds `getTermCols` and `getTermLines` to the base library. They return the
size of the terminal if either stdin or stdout is a tty.
* The `Data.List1` functions `foldr1` and `foldr1By` are now `public export`.
#### System
* Changes `getNProcessors` to return the number of online processors rather than

4
libs/base/Data/List1.idr
View File

@ -47,7 +47,7 @@ init (x ::: xs) = loop x xs where
loop x [] = []
loop x (y :: xs) = x :: loop y xs
export
public export
foldr1By : (func : a -> b -> b) -> (map : a -> b) -> (l : List1 a) -> b
foldr1By f map (x ::: xs) = loop x xs where
loop : a -> List a -> b
@ -58,7 +58,7 @@ public export
foldl1By : (func : b -> a -> b) -> (map : a -> b) -> (l : List1 a) -> b
foldl1By f map (x ::: xs) = foldl f (map x) xs
export
public export
foldr1 : (func : a -> a -> a) -> (l : List1 a) -> a
foldr1 f = foldr1By f id