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.
Should this change go in the CHANGELOG?
[x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).
Description
This makes it possible to call the function in more situations. It also brings its signature in line with the overloads on
List,List1andSnocList.The previous implementation of
Data.Vect.Elem.dropElemrequired the length of theVectto be available at runtime. This was used in order to recurse in the case that theElemis notHere. However, it turns out that this is not actually necessary. Idris can deduce that the tail must be non-empty if it contains anElem.Should this change go in the CHANGELOG?
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).