From badf1e98c8812e8b54258754cf47782f61d8fb15 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 6 Aug 2023 15:04:06 -0700 Subject: [PATCH] [ base ] Make foldr1 and foldr1By public --- CHANGELOG.md | 2 ++ libs/base/Data/List1.idr | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fc70675b43..6b4c543ee0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr index a34da95fd9..1b02fb5cbc 100644 --- a/libs/base/Data/List1.idr +++ b/libs/base/Data/List1.idr @@ -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