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

fix(base): runtime-erase implicit length argument to Vect's dropElem.

Browse Source 
This makes it possible to call the function in more situations. It also
brings its signature in line with the overloads on `List`, `List1` and
`SnocList`.

The previous implementation of `Data.Vect.Elem.dropElem` required the
length of the `Vect` to be available at runtime. This was used in order
to recurse in the case that the `Elem` is not `Here`. However, it turns
out that this is not actually necessary. Idris can deduce that the tail
must be non-empty if it contains an `Elem`.
This commit is contained in:
troiganto 2024-05-23 10:09:11 -05:00 committed by G. Allais
parent 1522c3a92c
commit e0b9a027e7
2 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
CHANGELOG_NEXT.md
View File

@ -154,6 +154,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
* Moved definition of `Data.Vect.nubBy` to the global scope as `nubByImpl` to
allow compile time proofs on `nubBy` and `nub`.
* Removed need for the runtime value of the implicit length argument in
`Data.Vect.Elem.dropElem`.
#### Contrib
* `Data.List.Lazy` was moved from `contrib` to `base`.

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

@ -94,9 +94,9 @@ mapElem (There e) = There (mapElem e)
||| @xs The vector to be removed from
||| @p A proof that the element to be removed is in the vector
public export
dropElem : {k : _} -> (xs : Vect (S k) t) -> Elem x xs -> Vect k t
dropElem (x::ys) Here = ys
dropElem {k = S k} (x::ys) (There later) = x :: dropElem ys later
dropElem : (xs : Vect (S k) t) -> Elem x xs -> Vect k t
dropElem (x::ys) Here = ys
dropElem (x::ys@(_::_)) (There later) = x :: dropElem ys later
||| Erase the indices, returning the bounded numeric position of the element
public export