Skip to content

Vec.Properties: drop eq parameter when it is a property (v3.0 changes)#2431

Draft
mildsunrise wants to merge 5 commits into
agda:masterfrom
mildsunrise:vec-drop-eq-v3
Draft

Vec.Properties: drop eq parameter when it is a property (v3.0 changes)#2431
mildsunrise wants to merge 5 commits into
agda:masterfrom
mildsunrise:vec-drop-eq-v3

Conversation

@mildsunrise

Copy link
Copy Markdown
Contributor

Follow up to #2430 with the changes for v3. See #2421 for context.

@mildsunrise mildsunrise changed the title Vec.Properties: drop eq parameter when it is a property Vec.Properties: drop eq parameter when it is a property (v3.0 changes) Jul 5, 2024
@Taneb

Taneb commented Jul 1, 2026

Copy link
Copy Markdown
Member

@mildsunrise now that the next release will be 3.0, do you want to revisit this?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants