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.

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

Migrate contrib:Data.Vect.Views.Extra to base:Data.Vect.Views #3497

Merged
merged 2 commits into from
Feb 22, 2025

Conversation

SlayerOfTheBad
Copy link
Contributor

Description

Moves Data.Vect.Views.Extra to Data.Vect.Views.
This mirrors the structure of Data.List.Views, and is consistent with the location mentioned in TDDwI.

Should this change go in the CHANGELOG?

Yes (Has already been added)

This mirrors the structure of Data.List.Views, and is consistent with
the location mentioned in TDDwI.
@mattpolzin
Copy link
Collaborator

This looks about right to me. Something administrative went wrong with the CI though there could also be a GitHub bug behind it so we'll hold off on merging for a minute and see if that works itself out.

@mattpolzin mattpolzin merged commit 34ccd1e into idris-lang:main Feb 22, 2025
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants