| .. |
|
Nat
|
fix: make rw collect only new goals, occurs check (#10306)
|
2025-09-14 04:44:55 +00:00 |
|
Sort
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
Attach.lean
|
chore: missing grind modifiers and local grind theorems config (#10428)
|
2025-09-17 16:15:16 +00:00 |
|
Basic.lean
|
feat: redefine String, part one (#10304)
|
2025-09-18 11:36:52 +00:00 |
|
BasicAux.lean
|
refactor: module-ize Std.Data.DHashMap (#9098)
|
2025-07-02 10:00:17 +00:00 |
|
Control.lean
|
feat: Add List.zipWithM and Array.zipWithM (#9528)
|
2025-07-28 08:39:52 +00:00 |
|
Count.lean
|
chore: more review of @[grind] annotations (#10340)
|
2025-09-11 06:09:52 +00:00 |
|
Erase.lean
|
chore: fix remainining discrepancies for change in grind pattern heuristics (#10347)
|
2025-09-11 12:48:52 +00:00 |
|
Find.lean
|
chore: fix remainining discrepancies for change in grind pattern heuristics (#10347)
|
2025-09-11 12:48:52 +00:00 |
|
FinRange.lean
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
Impl.lean
|
chore: @[expose] List.filterMapTR (#9793)
|
2025-08-08 04:55:38 +00:00 |
|
Lemmas.lean
|
chore: add grind annotations for List.not_mem_nil (#10493)
|
2025-09-22 12:18:03 +00:00 |
|
Lex.lean
|
feat: high-level order typeclasses (#9729)
|
2025-08-11 14:55:17 +00:00 |
|
MapIdx.lean
|
chore: @[expose] List.mapIdxM (#9794)
|
2025-08-08 04:55:50 +00:00 |
|
MinMax.lean
|
feat: improvements to Min/Max-related classes (#10024)
|
2025-08-22 07:08:00 +00:00 |
|
Monadic.lean
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
Nat.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
Notation.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
OfFn.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
Pairwise.lean
|
feat: redefine String, part one (#10304)
|
2025-09-18 11:36:52 +00:00 |
|
Perm.lean
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
Range.lean
|
feat: More grind annotations for List.range' (#9766)
|
2025-08-13 09:27:48 +00:00 |
|
Sort.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
Sublist.lean
|
chore: missing grind modifiers and local grind theorems config (#10428)
|
2025-09-17 16:15:16 +00:00 |
|
TakeDrop.lean
|
chore: avoid confusing public import all combination (#10051)
|
2025-08-22 12:04:42 +00:00 |
|
ToArray.lean
|
chore: reorganize Init imports around strings (#10289)
|
2025-09-07 17:09:14 +00:00 |
|
ToArrayImpl.lean
|
chore: [match_pattern] should enforce [expose] (#9534)
|
2025-07-31 11:51:47 +00:00 |
|
Zip.lean
|
chore: remove grind annotations of List/Array/Vector.zip_map_left/right (#10163)
|
2025-08-28 10:38:50 +00:00 |
