Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 1 commit into from
Jun 5, 2024
Merged

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

merged 1 commit into from
Jun 5, 2024

Commits on Jun 5, 2024

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

    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`.
    troiganto committed Jun 5, 2024
    Configuration menu
    Copy the full SHA
    9ea2833 View commit details
    Browse the repository at this point in the history