Skip to content

Add Data.Set.arbitraryElementOf.

Gijs Alberts requested to merge arbitrary-element-of-set into master

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

Merge request reports