Add Data.Set.arbitraryElementOf.
What does this MR do?
Adds Data.Set.arbitraryElementOf
. (retrieves an arbitrary element from the set).
After this is merged I will make an MR on containers.
Updates the CI/devcontainer images.
Related issues
Changes to public APIs
Author's checklist (required)
See CONTRIBUTING.md for the rationale behind these items:
-
The commit history does not contain merges (use git rebase -i master
if it does) -
Intermediate commits compile (use git rebase -i master
if not) -
Newly added code follows the Platform code style -
Newly added code is documented -
If bugs have been solved, tests have been added -
Appropriate types have been used, especially in APIs -
If efficiency is part of the acceptance criteria of the issue, a benchmark is provided -
A changelog entry has been added if required. See CONTRIBUTING.md
Edited by Gijs Alberts