From 7e72f9d2f436f0bb87a7655d514012b0a37b64ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Tue, 8 Oct 2019 21:16:41 +0200 Subject: [PATCH] Add some missing public exports --- libs/base/Data/Vect.idr | 2 +- libs/prelude/Prelude.idr | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index fa18ea0..05e9631 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -17,7 +17,7 @@ data Vect : (len : Nat) -> (elem : Type) -> Type where -- Hints for interactive editing %name Vect xs,ys,zs,ws -export +public export length : (xs : Vect len elem) -> Nat length [] = 0 length (x::xs) = 1 + length xs diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 5c8b571..6cd7641 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -1308,9 +1308,11 @@ Cast Nat Double where -- RANGES -- ------------ +public export countFrom : n -> (n -> n) -> Stream n countFrom start diff = start :: countFrom (diff start) diff +public export partial takeUntil : (n -> Bool) -> Stream n -> List n takeUntil p (x :: xs)