max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Std/Data
History
Paul Reichert 1448493489
feat: improvements to Min/Max-related classes (#10024) 
This PR adds useful declarations to the `LawfulOrderMin/Max` and
`LawfulOrderLeftLeaningMin/Max` API. In particular, it introduces
`.leftLeaningOfLE` factories for `Min` and `Max`. It also renames
`LawfulOrderMin/Max.of_le` to .of_le_min_iff` and `.of_max_le_iff` and
introduces a second variant with different arguments.
2025-08-22 07:08:00 +00:00
..
DHashMap chore: eliminate uses of intros x y z (#9983) 2025-08-19 06:09:13 +00:00
DTreeMap feat: integrate high-level order typeclasses with BEq and Ord (#9908) 2025-08-19 07:54:53 +00:00
ExtDHashMap feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
ExtDTreeMap feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
ExtHashMap feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
ExtHashSet feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
ExtTreeMap feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
ExtTreeSet feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
HashMap feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
HashSet feat: tree map lemmas for filter, map, filterMap (#9632) 2025-08-18 12:13:52 +00:00
Internal feat: improvements to Min/Max-related classes (#10024) 2025-08-22 07:08:00 +00:00
Iterators feat: high-level order typeclasses (#9729) 2025-08-11 14:55:17 +00:00
TreeMap feat: integrate high-level order typeclasses with BEq and Ord (#9908) 2025-08-19 07:54:53 +00:00
TreeSet feat: integrate high-level order typeclasses with BEq and Ord (#9908) 2025-08-19 07:54:53 +00:00
DHashMap.lean refactor: module-ize Std.Data.DHashMap (#9098) 2025-07-02 10:00:17 +00:00
DTreeMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtDHashMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtDTreeMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtHashMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtHashSet.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtTreeMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
ExtTreeSet.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
HashMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
HashSet.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Iterators.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
TreeMap.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
TreeSet.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00