| .. |
|
Nat
|
chore: preparation for Array.erase lemmas (#6836)
|
2025-01-29 04:07:51 +00:00 |
|
Sort
|
feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)
|
2025-01-28 23:34:30 +00:00 |
|
Attach.lean
|
feat: align {List/Array/Vector}.{attach,attachWith,pmap} lemmas (#6723)
|
2025-01-21 06:36:36 +00:00 |
|
Basic.lean
|
chore: remove unnecessary simp priorities (#6812)
|
2025-01-28 23:50:33 +00:00 |
|
BasicAux.lean
|
feat: replace List.lt with List.Lex (#6379)
|
2024-12-15 08:22:39 +00:00 |
|
Control.lean
|
feat: partial_fixpoint: partial functions with equations (#6355)
|
2025-01-21 09:54:30 +00:00 |
|
Count.lean
|
feat: align List/Array/Vector.count theorems (#6712)
|
2025-01-20 10:20:16 +00:00 |
|
Erase.lean
|
chore: preparation for Array.erase lemmas (#6836)
|
2025-01-29 04:07:51 +00:00 |
|
Find.lean
|
chore: preparation for Array.erase lemmas (#6836)
|
2025-01-29 04:07:51 +00:00 |
|
FinRange.lean
|
feat: upstream List.finRange from Batteries (#6234)
|
2024-11-27 04:27:22 +00:00 |
|
Impl.lean
|
feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)
|
2025-01-28 23:34:30 +00:00 |
|
Lemmas.lean
|
feat: finish aligning List/Array/Vector.ofFn lemmas (#6838)
|
2025-01-29 04:53:33 +00:00 |
|
Lex.lean
|
fix: ensure simp and dsimp do not unfold too much (#6397)
|
2024-12-21 04:16:15 +00:00 |
|
MapIdx.lean
|
feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)
|
2025-01-28 23:34:30 +00:00 |
|
MinMax.lean
|
feat: replace List.lt with List.Lex (#6379)
|
2024-12-15 08:22:39 +00:00 |
|
Monadic.lean
|
feat: lemmas about lexicographic order on Array and Vector (#6399)
|
2024-12-19 10:36:50 +00:00 |
|
Nat.lean
|
feat: Array.swap_perm (#6272)
|
2024-12-01 08:35:28 +00:00 |
|
Notation.lean
|
feat: lemmas about Std.Range (#6396)
|
2024-12-16 03:16:46 +00:00 |
|
OfFn.lean
|
feat: finish aligning List/Array/Vector.ofFn lemmas (#6838)
|
2025-01-29 04:53:33 +00:00 |
|
Pairwise.lean
|
feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932)
|
2024-11-03 16:23:37 +00:00 |
|
Perm.lean
|
chore: fix signature of perm_insertIdx (#6532)
|
2025-01-04 23:43:23 +00:00 |
|
Range.lean
|
feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)
|
2025-01-28 23:34:30 +00:00 |
|
Sort.lean
|
feat: List.mergeSort (#5092)
|
2024-08-20 06:32:52 +00:00 |
|
Sublist.lean
|
chore: robustify for byAsSorry (#6287)
|
2024-12-02 23:53:16 +00:00 |
|
TakeDrop.lean
|
chore: remove deprecations from 2024-06 (#6696)
|
2025-01-19 08:46:24 +00:00 |
|
ToArray.lean
|
chore: preparation for Array.erase lemmas (#6836)
|
2025-01-29 04:07:51 +00:00 |
|
ToArrayImpl.lean
|
chore: alignment of Array and List lemmas (#6342)
|
2024-12-09 11:30:45 +00:00 |
|
Zip.lean
|
feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)
|
2025-01-28 23:34:30 +00:00 |
