Commit 2023-10-20 19:41 142eedb5
View on Github →chore: Remove DiscrTree.getElements, use std4’s .values (#7800)
it duplicates a definition found in std4.
In fact, it duplicates two definitions found in std4, so use
.values consistently, so that .elements can be dropped from std4
(in https://github.com/leanprover/std4/pull/285).