Rob23oba
688b930bad
feat: tree map lemmas for filter, map, filterMap ( #9632 )
...
This PR adds lemmas for the `TreeMap` operations `filter`, `map` and
`filterMap`. These lemmas existed already for hash maps and are simply
ported over from there.
2025-08-18 12:13:52 +00:00
Sebastian Ullrich
e5730e9b7e
refactor: module-ize remainder of Std ( #9195 )
2025-07-17 11:43:57 +00:00
Kim Morrison
c52605dfe3
fix: some inconsistencies in Map grind annotations ( #9054 )
...
This PR corrects some inconsistencies in `TreeMap`/`HashMap` grind
annotations, for `isSome_get?_eq_contains` and `empty_eq_emptyc`.
2025-06-28 06:41:19 +00:00
Kim Morrison
38ca310fb7
feat: @[grind] annotations for TreeMap ( #8446 )
...
This PR adds basic `@[grind]` annotations for `TreeMap` and its
variants. Likely more annotations will be added after we've explored
some examples.
2025-05-24 04:49:54 +00:00
Kim Morrison
37529a5518
chore: initial work on grind attributes for TreeMap ( #8342 )
2025-05-15 02:24:51 +00:00
Kim Morrison
7688fbb067
feat: add @[grind] annotations to contains_iff_mem lemmas ( #8328 )
...
This PR adds the `@[grind =]` attribute to all `contains_iff_mem`
lemmas.
2025-05-14 00:03:46 +00:00
Kim Morrison
29cc75531a
chore: remove accidental grind trace options ( #8311 )
2025-05-13 05:58:46 +00:00
Kim Morrison
a08d182359
feat: add @[grind] annotations for HashMap ( #8246 )
...
This PR add `@[grind]` annotations for HashMap and variants.
2025-05-13 04:56:41 +00:00
Kim Morrison
6e2e1a4f89
chore: consistently add @[simp] to getKey_eq map lemmas ( #8186 )
...
These lemmas were inconsistently marked as `@[simp]`, but they seem
generally useful, so this uniformly marks this lemmas as `@[simp]` for
all map variants.
2025-05-03 16:12:33 +00:00
Kim Morrison
34d944c4a9
feat: add ofList_eq_insertMany_empty lemmas for map types ( #8182 )
...
This PR adds `ofList_eq_insertMany_empty` lemmas for all the hash/tree
map types, with the exception of
`Std.HashSet.Raw.ofList_eq_insertMany_empty`.
2025-05-02 17:16:23 +00:00
Kim Morrison
1d5110e140
feat: insertMany_append lemmas for map variants ( #8184 )
...
This PR adds the `insertMany_append` lemma for all map variants.
2025-04-30 17:09:51 +00:00
Kim Morrison
d10d17ce03
chore: add HashMap/TreeMap.isSome_X simp lemmas ( #8143 )
...
These lemmas were previously only stated the other way round, but in
this direction they are both good simp lemmas, and good grind lemmas.
2025-04-28 13:48:06 +00:00
Rob23oba
747ea853b5
feat: extensional hash maps ( #8004 )
...
This PR adds extensional hash maps and hash sets under the names
`Std.ExtDHashMap`, `Std.ExtHashMap` and `Std.ExtHashSet`. Extensional
hash maps work like regular hash maps, except that they have
extensionality lemmas which make them easier to use in proofs. This
however makes it also impossible to regularly iterate over its entries.
2025-04-28 06:48:25 +00:00
