diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-19 17:03:45 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-19 17:03:45 +0200 |
| commit | 4d67d2e1597d1ed976fb4d1eb0062171925a45cb (patch) | |
| tree | 0fc6a5296b8cbc9933d0b6e638acdae04190e1b7 /Common/Helpers.lean | |
| parent | fa9074b17a6afc73cdf1854da222ba961fc1cc5c (diff) | |
Make CompleteTree.heapRemoveLast private.
It's confusing, because it uses breadth-first indexing, and regular
indices are depth-first.
Also, it's not needed in the public API, as there is the removeAt
function that can do the same.
Diffstat (limited to 'Common/Helpers.lean')
0 files changed, 0 insertions, 0 deletions