diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-19 17:06:50 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-19 17:06:50 +0200 |
| commit | b22f0f04c6fdf378a4c586cab657975f7d49f992 (patch) | |
| tree | 7504772f5909d51e62278a82de4118ad19ae19ca /Common/Helpers.lean | |
| parent | 4d67d2e1597d1ed976fb4d1eb0062171925a45cb (diff) | |
Heap: Further nomenclature improvements.
Diffstat (limited to 'Common/Helpers.lean')
0 files changed, 0 insertions, 0 deletions