idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

Remove dependency to Vector length in deleteAt

Browse Source
This commit is contained in:
Nicolas Biri 2020-07-14 08:25:46 +02:00 committed by G. Allais
parent 7920eb8a0e
commit aba76206c9
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -111,9 +111,10 @@ insertAt (FS k) y (x::xs) = x :: insertAt k y xs
||| deleteAt 1 [1,2,3,4]
||| ```
public export
deleteAt : {len : _} -> Fin (S len) -> Vect (S len) elem -> Vect len elem
deleteAt FZ (_::xs) = xs
deleteAt {len = S _} (FS k) (x::xs) = x :: deleteAt k xs
deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
deleteAt FZ (_::xs) = xs
deleteAt (FS k) [x] = absurd k
deleteAt (FS k) (x::xs@(_::_)) = x :: deleteAt k xs
||| Replace an element at a particlar index with another
|||