| .. |
|
Lex
|
chore: protect some lemmas in List/Array/Vector namespace (#6425)
|
2024-12-20 11:23:56 +00:00 |
|
Subarray
|
feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)
|
2024-11-24 07:59:57 +00:00 |
|
Attach.lean
|
feat: align {List/Array/Vector}.{attach,attachWith,pmap} lemmas (#6723)
|
2025-01-21 06:36:36 +00:00 |
|
Basic.lean
|
feat: align List/Array/Vector.count theorems (#6712)
|
2025-01-20 10:20:16 +00:00 |
|
BasicAux.lean
|
chore: run Batteries linter on Lean (#6364)
|
2024-12-13 01:28:53 +00:00 |
|
BinSearch.lean
|
feat: remove partial keyword and runtime bounds checks from Array.binSearch (#6193)
|
2024-11-24 06:08:16 +00:00 |
|
Bootstrap.lean
|
feat: align List/Array/Vector flatten lemmas (#6640)
|
2025-01-15 01:16:19 +00:00 |
|
Count.lean
|
feat: align List/Array/Vector.count theorems (#6712)
|
2025-01-20 10:20:16 +00:00 |
|
DecidableEq.lean
|
chore: run Batteries linter on Lean (#6364)
|
2024-12-13 01:28:53 +00:00 |
|
Find.lean
|
feat: align List/Array/Vector flatten lemmas (#6640)
|
2025-01-15 01:16:19 +00:00 |
|
FinRange.lean
|
feat: upstream List.finRange from Batteries (#6234)
|
2024-11-27 04:27:22 +00:00 |
|
GetLit.lean
|
feat: relate Array.takeWhile with List.takeWhile (#5950)
|
2024-11-05 05:05:53 +00:00 |
|
InsertionSort.lean
|
feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)
|
2024-11-24 07:59:57 +00:00 |
|
Lemmas.lean
|
feat: align {List/Array/Vector}.{attach,attachWith,pmap} lemmas (#6723)
|
2025-01-21 06:36:36 +00:00 |
|
Lex.lean
|
feat: lemmas about lexicographic order on Array and Vector (#6399)
|
2024-12-19 10:36:50 +00:00 |
|
MapIdx.lean
|
feat: complete alignment of {List,Array,Vector}.{mapIdx,mapFinIdx} (#6701)
|
2025-01-20 04:06:37 +00:00 |
|
Mem.lean
|
feat: change Array.get to take a Nat and a proof (#6032)
|
2024-11-12 03:30:46 +00:00 |
|
Monadic.lean
|
feat: lemmas about lexicographic order on Array and Vector (#6399)
|
2024-12-19 10:36:50 +00:00 |
|
Perm.lean
|
feat: Array.swap_perm (#6272)
|
2024-12-01 08:35:28 +00:00 |
|
QSort.lean
|
feat: remove runtime bounds checks and partial from qsort (#6241)
|
2024-12-01 06:26:00 +00:00 |
|
Set.lean
|
feat: rename Array.setD to setIfInBounds (#6195)
|
2024-11-24 08:54:19 +00:00 |
|
Subarray.lean
|
chore: remove >6 month old deprecations (#6057)
|
2024-11-13 23:21:23 +00:00 |
|
TakeDrop.lean
|
chore: cleanup of Array lemmas (#6337)
|
2024-12-08 22:03:23 +00:00 |
91bae2e064