Skip to content

[ add ] more properties of Data.List.Relation.Unary.All.Null - #3091

Open
jamesmckinna wants to merge 3 commits into
agda:masterfrom
jamesmckinna:add-Null-properties
Open

[ add ] more properties of Data.List.Relation.Unary.All.Null#3091
jamesmckinna wants to merge 3 commits into
agda:masterfrom
jamesmckinna:add-Null-properties

Conversation

@jamesmckinna

Copy link
Copy Markdown
Collaborator

Prompted by #3084 these seem the most important additions to make.

@jamesmckinna jamesmckinna added this to the v3.0 milestone Jul 26, 2026
Comment thread src/Data/List/Relation/Unary/All/Properties.agda Outdated
@silas-hw

Copy link
Copy Markdown
Contributor

Should this be merged first and then rebased/merged into #3084?

@jamesmckinna

jamesmckinna commented Jul 27, 2026

Copy link
Copy Markdown
Collaborator Author

Should this be merged first and then rebased/merged into #3084?

Well, that's one way to go but up to the reviewers. V3.0 is a moving target, so some refactoring/rebasing is... inevitable before the 'new' contributions stabilise. It'll all come out in the wash ... so no need to commit one way or another right now!

UPDATED that said, @silas-hw

  • I'd be happy for these to merged sooner, and then you could use the lemmas, rather than have to replicate them as in the current evolution of Add Queue datatype #3084
  • in general, if you find in the course of developing such a PR that you need additional 'infrastructure' lemmas in other parts of the library, you should feel free to make such things part of the PR; but there's always inevitably some judgment call to make about what/where/when with such refactoring...

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

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants