add search function to Data.List.Relation.Unary.All

[jamesmckinna]

Fixes #989

NB. UPDATED CHANGELOG added

• In Data.List.Relation.Unary.All:

  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs

[JacquesCarette]

I'd approve if there were a CHANGELOG.

[jamesmckinna]

I'd approve if there were a CHANGELOG.

Currently all the v2.2-badged PRs I'm posting (or reviewing ;-)) are without CHANGELOG, against the inevitable reset after the eventual v2.1 release...

[mildsunrise]

maybe it would ease some burden for everyone if we started special branches for every release, i.e. v2.1, and we could keep working on master for the next minor (or even major) release?

[jamesmckinna]

maybe it would ease some burden for everyone if we started special branches for every release, i.e. v2.1, and we could keep working on master for the next minor (or even major) release?

That sounds good, so shoutout to the release-Meister @MatthewDaggitt for comment!? (The actual machinery of producing a release is still a bit mysterious to me...)

[Taneb]

Approved pending changelog

[MatthewDaggitt]

Yup happy to create a release branch. We've never really had the quantity of contributors around a release time that made it a necessity before.

[jamesmckinna]

Yup happy to create a release branch. We've never really had the quantity of contributors around a release time that made it a necessity before.

But let's capitalise on the momentum that our new (and old!) contributors are bringing to the development process!?

[jamesmckinna]

Notwithstanding the approvals (for which all thanks), I'm wondering if a sharper lemma should (instead) be provable, namely that for Decidable P, we can exhibit a view of any given list xs as either All (not P) xs or All (not P) ys and Any P zs for a prefix decomposition ys ++ zs of xs (while trying to prove the equivalence of various definitions of deleteFirst against #988 ...)

... but such a thing could in any case have a 'better' name, such as prefixSearch or searchFirst, so could/should be orthogonal to this PR!?

[jamesmckinna]

CHANGELOG entry added on the blank v2.2-dev template inherited from #2439 ... so a successful merge of that PR should see a more sensible diff/patch for this one... and resolve the newly-introduced merge conflict ;-)/:-(