max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Std/Data
History
Kim Morrison 0fd516a1df
feat: add simpler getElem_map statements given LawfulBEq for all HashMap variants (#8188) 
This PR takes the existing `getElem_map` statements for `HashMap`
variants (also `getElem?`, `getElem!`, and `getD` statements), adds a
prime to their name and an explanatory comment, and replaces the
unprimed statement with a simpler statement that is only true with
`LawfulBEq` present. The original statements which were simp lemmas are
now low priority simp lemmas, so the nicer statements should fire when
`LawfulBEq` is available.
2025-05-02 17:16:35 +00:00
..
DHashMap feat: add simpler getElem_map statements given LawfulBEq for all HashMap variants (#8188) 2025-05-02 17:16:35 +00:00
DTreeMap feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
ExtDHashMap feat: add simpler getElem_map statements given LawfulBEq for all HashMap variants (#8188) 2025-05-02 17:16:35 +00:00
ExtHashMap feat: add simpler getElem_map statements given LawfulBEq for all HashMap variants (#8188) 2025-05-02 17:16:35 +00:00
ExtHashSet feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
HashMap feat: add simpler getElem_map statements given LawfulBEq for all HashMap variants (#8188) 2025-05-02 17:16:35 +00:00
HashSet feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
Internal feat: lemmas about List/Array/Vector.contains (#8175) 2025-04-30 14:38:56 +00:00
TreeMap feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
TreeSet feat: add ofList_eq_insertMany_empty lemmas for map types (#8182) 2025-05-02 17:16:23 +00:00
DHashMap.lean fix: unorphan modules in Std.Data (#4679) 2024-07-08 07:57:56 +00:00
DTreeMap.lean fix: import all raw tree map modules into Std.Data (#8044) 2025-04-24 10:06:32 +00:00
ExtDHashMap.lean feat: extensional hash maps (#8004) 2025-04-28 06:48:25 +00:00
ExtHashMap.lean feat: extensional hash maps (#8004) 2025-04-28 06:48:25 +00:00
ExtHashSet.lean feat: extensional hash maps (#8004) 2025-04-28 06:48:25 +00:00
HashMap.lean feat: Std.HashMap (#4583) 2024-07-05 10:14:20 +00:00
HashSet.lean feat: Std.HashMap (#4583) 2024-07-05 10:14:20 +00:00
TreeMap.lean fix: import all raw tree map modules into Std.Data (#8044) 2025-04-24 10:06:32 +00:00
TreeSet.lean chore: USE_LAKE: integrate into CMake (#4466) 2025-03-15 08:58:01 +00:00