lean4-htt/src/Std/Data/DHashMap/Internal
Paul Reichert 9a3fb90e40
refactor: replace Iter(M).size with Iter(M).count (#10952)
This PR replaces `Iter(M).size` with the `Iter(M).count`. While the
former used a special `IteratorSize` type class, the latter relies on
`IteratorLoop`. The `IteratorSize` class is deprecated. The PR also
renames lemmas about ranges be replacing `_Rcc` with `_rcc`, `_Rco` with
`_roo` (and so on) in names, in order to be more consistent with the
naming convention.
2025-11-12 16:41:00 +00:00
..
AssocList refactor: replace Iter(M).size with Iter(M).count (#10952) 2025-11-12 16:41:00 +00:00
Defs.lean chore: >6 month old deprecations (#10969) 2025-10-26 22:48:41 +00:00
HashesTo.lean perf: shorten critical build path around String.Basic (#10614) 2025-09-29 19:45:21 +00:00
Index.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Model.lean chore: >6 month old deprecations (#10969) 2025-10-26 22:48:41 +00:00
Raw.lean feat: redefine HashSet.union and add lemmas (#10611) 2025-10-16 08:43:01 +00:00
RawLemmas.lean feat: add union on ExtDHashMap/ExtHashMap/ExtHashSet (#10946) 2025-11-10 13:48:36 +00:00
WF.lean chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00