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

Add drop for Vect.

Browse Source
This commit is contained in:
Mathew Polzin 2021-06-09 08:31:23 -07:00 committed by G. Allais
parent 4a0a5759b8
commit bdd8f4157b
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -87,6 +87,12 @@ take : (n : Nat)
take 0 xs = Nil
take (S k) (x :: xs) = x :: take k xs
||| Drop the first `n` elements of a Vect.
drop : (n : Nat) -> Vect l elem -> Vect (l `minus` n) elem
drop 0 xs = rewrite minusZeroRight l in xs
drop (S k) [] = rewrite minusZeroLeft (S k) in []
drop (S k) (x :: xs) = drop k xs
||| Extract a particular element from a vector
|||
||| ```idris example