edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-02 17:52:09 +03:00
Code Issues Projects Releases Wiki Activity

Add some missing public exports

Browse Source
This commit is contained in:
Tim Süberkrüb 2019-10-08 21:16:41 +02:00
parent 85459814ef
commit 7e72f9d2f4
2 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/Vect.idr
View File

@ -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

2
libs/prelude/Prelude.idr
View File

@ -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)